diff -r 07e33cac5d9c -r 01d0c66ce523 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Wed Aug 02 16:07:32 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed Aug 02 16:49:26 2000 +0200
@@ -189,15 +189,15 @@
 local
 
 fun restart isar =
- (ThyInfo.touch_all_thys ();
-  if isar then tell_clear_goals () else kill_goal ();
+ (if isar then tell_clear_goals () else kill_goal ();
   tell_clear_response ();
   writeln (Session.welcome ()));
 
 in
 
-fun isa_restart () = restart false;
-fun isar_restart () = (restart true; raise Toplevel.RESTART);
+fun isa_start () = restart false;
+fun isa_restart () = (ThyInfo.touch_all_thys (); restart false);
+fun isar_restart () = (ThyInfo.touch_all_thys (); restart true; raise Toplevel.RESTART);
 
 end;
 
@@ -261,7 +261,7 @@
   ThmDeps.enable ();
   if isar then ml_prompts "ML> " "ML# "
   else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
-  if isar then Isar.sync_main () else isa_restart ());
+  if isar then Isar.sync_main () else isa_start ());