1.1 --- a/src/Pure/ROOT.ML	Tue Jan 16 00:33:40 2001 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Jan 16 00:34:31 2001 +0100
     1.3 @@ -82,5 +82,3 @@
     1.4  
     1.5  print_depth 8;
     1.6  ml_prompts "ML> " "ML# ";
     1.7 -
     1.8 -Session.finish ();