src/Pure/ROOT.ML
changeset 6237 699b4daf1451
parent 6226 42c94393d39e
child 6365 416c4679f937
     1.1 --- a/src/Pure/ROOT.ML	Fri Feb 05 17:31:42 1999 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Feb 05 20:56:50 1999 +0100
     1.3 @@ -74,8 +74,10 @@
     1.4  
     1.5  use "install_pp.ML";
     1.6  
     1.7 -val use = ThyInfo.load_file o Path.unpack;
     1.8 +val use = ThyInfo.use;
     1.9  val cd = File.cd o Path.unpack;
    1.10  
    1.11  print_depth 8;
    1.12  (*ml_prompts "ML> " "ML# ";*)
    1.13 +
    1.14 +Session.finish ();