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