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