diff -r d4af3f6fa997 -r fd5053c8a7ac src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Fri Sep 15 16:38:15 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Fri Sep 15 16:40:20 2000 +0200
@@ -270,13 +270,12 @@
   setup_messages ();
   setup_state ();
   setup_thy_loader ();
-  print_mode := [proof_generalN];
+  print_mode := proof_generalN :: ! print_mode;
   set quick_and_dirty;
   ThmDeps.enable ();
   if isar then ml_prompts "ML> " "ML# "
   else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
-  welcome ();
-  if isar then Isar.sync_main () else isa_start ());
+  if isar then (welcome (); Isar.sync_main ()) else isa_start ());