# HG changeset patch
# User wenzelm
# Date 1199565441 -3600
# Node ID 54373fa3bd75fa1b9371f139aeb6c97129fa9b74
# Parent  00b2a1b2c4e934bc05da50bd66c6a7a2444bd3b5
secure_main: removed separate welcome;

diff -r 00b2a1b2c4e9 -r 54373fa3bd75 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;