# HG changeset patch
# User wenzelm
# Date 940616719 -7200
# Node ID b284079cd902b753a37a701b9a082bc2f699d277
# Parent  56a84b4d04b12e74d59c17cebab28d7cf806923a
tuned repeat_undo;

diff -r 56a84b4d04b1 -r b284079cd902 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Fri Oct 22 20:25:00 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Fri Oct 22 20:25:19 1999 +0200
@@ -175,8 +175,11 @@
 fun kill_goal () =
   (Goals.reset_goals (); writeln "Proof General, please clear the goals buffer.");
 
+fun no_print_goals f = setmp print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
+
 fun repeat_undo 0 = ()
-  | repeat_undo n = (undo(); repeat_undo (n - 1));
+  | repeat_undo 1 = undo ()
+  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
 
 fun isa_restart () =
  (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");