1local
2   open HolKernel boolLib bossLib;
3   val holfoot_base_dir = Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/";
4   val use_polyml = (Systeml.ML_SYSNAME = "poly") andalso
5     (Lib.mem "holfoot.state" (Portable.listDir (holfoot_base_dir^"poly")) handle SysErr _ => false)
6   val mldir = if use_polyml then "poly" else "mosml";
7   val usefile = concat [holfoot_base_dir, mldir, "/header.sml"];
8in
9   val _ = use usefile;
10end;
11