Symbol.use (eliminated Use.exit_use);
authorwenzelm
Thu, 04 Feb 1999 18:17:01 +0100
changeset 6230 85fc589a66ea
parent 6229 f839b261b87f
child 6231 438a642ee92d
Symbol.use (eliminated Use.exit_use);
src/Pure/Thy/session.ML
--- a/src/Pure/Thy/session.ML	Thu Feb 04 18:16:22 1999 +0100
+++ b/src/Pure/Thy/session.ML	Thu Feb 04 18:17:01 1999 +0100
@@ -48,9 +48,14 @@
 fun finish () = (ThyInfo.finish_all (); session_finished := true);
 
 
-(* use_dir *)	(* FIXME info *)
+(* use_dir *)
+
+val root_file = ThyLoad.ml_path "ROOT";
 
-fun use_dir reset info name = (init reset name; Use.exit_use "ROOT.ML"; finish ());
+fun use_dir reset info name =
+  (init reset name;
+    Symbol.use root_file handle _ => exit 1;
+    finish ());
 
 
 end;