--- 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 ());