# HG changeset patch
# User wenzelm
# Date 1167478407 -3600
# Node ID 4e44e74dc7e751a4a942014048b0d52206366cee
# Parent  2cbee05b18a10a51417b43aed4bb8c7fe5c9130c
Toplevel.init_state;

diff -r 2cbee05b18a1 -r 4e44e74dc7e7 src/Pure/Isar/outer_syntax.ML
--- 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);
 
diff -r 2cbee05b18a1 -r 4e44e74dc7e7 src/Pure/Isar/session.ML
--- 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);