Session.finish ();
authorwenzelm
Fri Feb 05 20:56:50 1999 +0100 (1999-02-05)
changeset 6237699b4daf1451
parent 6236 958f4fc3e8b8
child 6238 bd7b4a23118f
Session.finish ();
use;
src/Pure/ROOT.ML
     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 ();