Toplevel.actual_proof;

--- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 13 16:07:33 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 13 16:07:34 2005 +0200
@@ -131,10 +131,14 @@
 
 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
 val clear_undos_theory = Toplevel.history o History.clear;
-val redo = Toplevel.history History.redo o Toplevel.proof'' ProofHistory.redo o
+
+val redo =
+  Toplevel.history History.redo o
+  Toplevel.actual_proof ProofHistory.redo o
   Toplevel.skip_proof History.redo;
 
-fun undos_proof n = Toplevel.proof'' (fn prf =>
+fun undos_proof n =
+  Toplevel.actual_proof (fn prf =>
     if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o
   Toplevel.skip_proof (fn h =>
     if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h);

--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 13 16:07:33 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 13 16:07:34 2005 +0200
@@ -359,7 +359,7 @@
 
 val haveP =
   OuterSyntax.command "have" "state local goal" K.prf_goal
-    (statement >> ((Toplevel.print oo Toplevel.proof) o  IsarThy.have));
+    (statement >> ((Toplevel.print oo Toplevel.proof) o IsarThy.have));
 
 val thusP =
   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
@@ -501,7 +501,8 @@
 
 val proofP =
   OuterSyntax.command "proof" "backward proof" K.prf_block
-    (Scan.option P.method >> (fn m => Toplevel.print o Toplevel.proof (IsarThy.proof m) o
+    (Scan.option P.method >> (fn m => Toplevel.print o
+      Toplevel.actual_proof (IsarThy.proof m) o
       Toplevel.skip_proof (History.apply (fn i => i + 1))));