src/Pure/Isar/isar_thy.ML
changeset 8681 957a5fe9b212
parent 8615 419166fa66d0
child 8724 ef7efded8fdc
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Apr 06 19:11:30 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Apr 07 17:36:25 2000 +0200
     1.3 @@ -120,10 +120,10 @@
     1.4    val begin_block: ProofHistory.T -> ProofHistory.T
     1.5    val next_block: ProofHistory.T -> ProofHistory.T
     1.6    val end_block: ProofHistory.T -> ProofHistory.T
     1.7 -  val defer: int option -> ProofHistory.T -> ProofHistory.T
     1.8 -  val prefer: int -> ProofHistory.T -> ProofHistory.T
     1.9 -  val apply: Method.text -> ProofHistory.T -> ProofHistory.T
    1.10 -  val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
    1.11 +  val defer: int option * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.12 +  val prefer: int * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.13 +  val apply: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.14 +  val apply_end: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T
    1.15    val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
    1.16      -> ProofHistory.T -> ProofHistory.T
    1.17    val qed: (Method.text * Comment.interest) option * Comment.text
    1.18 @@ -355,14 +355,15 @@
    1.19  
    1.20  fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain;
    1.21  
    1.22 -fun defer i = ProofHistory.applys (shuffle Method.defer i);
    1.23 -fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
    1.24 +fun defer (i, comment_ignore) = ProofHistory.applys (shuffle Method.defer i);
    1.25 +fun prefer (i, comment_ignore) = ProofHistory.applys (shuffle Method.prefer i);
    1.26  
    1.27  
    1.28  (* backward steps *)
    1.29  
    1.30 -fun apply m = ProofHistory.applys (Method.refine m o Proof.assert_backward);
    1.31 -fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
    1.32 +fun apply (m, comment_ignore) = ProofHistory.applys (Method.refine m o Proof.assert_backward);
    1.33 +fun apply_end (m, comment_ignore) =
    1.34 +  ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
    1.35  
    1.36  val proof = ProofHistory.applys o Method.proof o
    1.37    apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;