--- a/src/Pure/Isar/outer_syntax.ML Sat Dec 30 12:33:26 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sat Dec 30 12:33:27 2006 +0100
@@ -318,7 +318,7 @@
ml_prompts "ML> " "ML# ");
fun gen_main term no_pos =
- (Toplevel.set_state Toplevel.toplevel;
+ (Toplevel.init_state ();
writeln (Session.welcome ());
gen_loop term no_pos);
--- a/src/Pure/Isar/session.ML Sat Dec 30 12:33:26 2006 +0100
+++ b/src/Pure/Isar/session.ML Sat Dec 30 12:33:27 2006 +0100
@@ -61,6 +61,7 @@
(Output.accumulated_time ();
ThyInfo.finish ();
Present.finish ();
+ Toplevel.init_state ();
session_finished := true);