Toplevel.actual_proof;
authorwenzelm
Wed Jul 13 16:07:34 2005 +0200 (2005-07-13)
changeset 16812c7d38e714768
parent 16811 23b9c52612db
child 16813 67140ae50e77
Toplevel.actual_proof;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 13 16:07:33 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 13 16:07:34 2005 +0200
     1.3 @@ -131,10 +131,14 @@
     1.4  
     1.5  fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
     1.6  val clear_undos_theory = Toplevel.history o History.clear;
     1.7 -val redo = Toplevel.history History.redo o Toplevel.proof'' ProofHistory.redo o
     1.8 +
     1.9 +val redo =
    1.10 +  Toplevel.history History.redo o
    1.11 +  Toplevel.actual_proof ProofHistory.redo o
    1.12    Toplevel.skip_proof History.redo;
    1.13  
    1.14 -fun undos_proof n = Toplevel.proof'' (fn prf =>
    1.15 +fun undos_proof n =
    1.16 +  Toplevel.actual_proof (fn prf =>
    1.17      if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o
    1.18    Toplevel.skip_proof (fn h =>
    1.19      if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h);
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jul 13 16:07:33 2005 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 13 16:07:34 2005 +0200
     2.3 @@ -359,7 +359,7 @@
     2.4  
     2.5  val haveP =
     2.6    OuterSyntax.command "have" "state local goal" K.prf_goal
     2.7 -    (statement >> ((Toplevel.print oo Toplevel.proof) o  IsarThy.have));
     2.8 +    (statement >> ((Toplevel.print oo Toplevel.proof) o IsarThy.have));
     2.9  
    2.10  val thusP =
    2.11    OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
    2.12 @@ -501,7 +501,8 @@
    2.13  
    2.14  val proofP =
    2.15    OuterSyntax.command "proof" "backward proof" K.prf_block
    2.16 -    (Scan.option P.method >> (fn m => Toplevel.print o Toplevel.proof (IsarThy.proof m) o
    2.17 +    (Scan.option P.method >> (fn m => Toplevel.print o
    2.18 +      Toplevel.actual_proof (IsarThy.proof m) o
    2.19        Toplevel.skip_proof (History.apply (fn i => i + 1))));
    2.20  
    2.21