# HG changeset patch
# User wenzelm
# Date 918244610 -3600
# Node ID 699b4daf14512b021cc34d1ff00469a50e38c647
# Parent  958f4fc3e8b8bc54d219bb6d6b50f8c867978e70
Session.finish ();
use;

diff -r 958f4fc3e8b8 -r 699b4daf1451 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 ();