1.1 --- a/src/Pure/Interface/proof_general.ML	Fri Oct 22 20:25:00 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Fri Oct 22 20:25:19 1999 +0200
     1.3 @@ -175,8 +175,11 @@
     1.4  fun kill_goal () =
     1.5    (Goals.reset_goals (); writeln "Proof General, please clear the goals buffer.");
     1.6  
     1.7 +fun no_print_goals f = setmp print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
     1.8 +
     1.9  fun repeat_undo 0 = ()
    1.10 -  | repeat_undo n = (undo(); repeat_undo (n - 1));
    1.11 +  | repeat_undo 1 = undo ()
    1.12 +  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
    1.13  
    1.14  fun isa_restart () =
    1.15   (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");