# HG changeset patch
# User wenzelm
# Date 918148621 -3600
# Node ID 85fc589a66ea925621609f6bf13dae35804cc9b5
# Parent  f839b261b87f9f93b884fa13d7ee41ad9ab6d4f5
Symbol.use (eliminated Use.exit_use);

diff -r f839b261b87f -r 85fc589a66ea 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;