src/Pure/ROOT.ML
changeset 6237 699b4daf1451
parent 6226 42c94393d39e
child 6365 416c4679f937
--- 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 ();