Session.finish ();
authorwenzelm
Fri, 05 Feb 1999 20:56:50 +0100
changeset 6237 699b4daf1451
parent 6236 958f4fc3e8b8
child 6238 bd7b4a23118f
Session.finish (); use;
src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Feb 05 17:31:42 1999 +0100
+++ b/src/Pure/ROOT.ML	Fri Feb 05 20:56:50 1999 +0100
@@ -74,8 +74,10 @@
 
 use "install_pp.ML";
 
-val use = ThyInfo.load_file o Path.unpack;
+val use = ThyInfo.use;
 val cd = File.cd o Path.unpack;
 
 print_depth 8;
 (*ml_prompts "ML> " "ML# ";*)
+
+Session.finish ();