secure_main: removed separate welcome;
authorwenzelm
Sat, 05 Jan 2008 21:37:21 +0100
changeset 25839 54373fa3bd75
parent 25838 00b2a1b2c4e9
child 25840 8a84f00f7139
secure_main: removed separate welcome;
src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Jan 05 21:37:20 2008 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Jan 05 21:37:21 2008 +0100
@@ -355,7 +355,7 @@
   fun loop () = gen_loop (Secure.is_secure ()) false;
   fun sync_main () = gen_main (Secure.is_secure ()) true;
   fun sync_loop () = gen_loop (Secure.is_secure ()) true;
-  fun secure_main () = gen_main true true;
+  fun secure_main () = (Toplevel.init_state (); gen_loop true true);
   val toplevel = Toplevel.program;
 end;