src/Pure/Isar/method.ML

--- a/src/Pure/Isar/method.ML	Wed May 26 22:44:41 1999 +0200
+++ b/src/Pure/Isar/method.ML	Wed May 26 22:45:08 1999 +0200
@@ -55,10 +55,14 @@
   val tac: text -> Proof.state -> Proof.state Seq.seq
   val then_tac: text -> Proof.state -> Proof.state Seq.seq
   val proof: text option -> Proof.state -> Proof.state Seq.seq
-  val local_qed: text option -> bool -> Proof.state -> Proof.state Seq.seq
-  val local_terminal_proof: text -> bool -> Proof.state -> Proof.state Seq.seq
-  val local_immediate_proof: bool -> Proof.state -> Proof.state Seq.seq
-  val local_default_proof: bool -> Proof.state -> Proof.state Seq.seq
+  val local_qed: text option -> ({kind: string, name: string, thm: thm} -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val local_terminal_proof: text -> ({kind: string, name: string, thm: thm} -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit)
+    -> Proof.state -> Proof.state Seq.seq
+  val local_default_proof: ({kind: string, name: string, thm: thm} -> unit)
+    -> Proof.state -> Proof.state Seq.seq
   val global_qed: bstring option -> theory attribute list option -> text option
     -> Proof.state -> theory * {kind: string, name: string, thm: thm}
   val global_terminal_proof: text -> Proof.state -> theory * {kind: string, name: string, thm: thm}
@@ -301,7 +305,7 @@
   |> Seq.map Proof.enter_forward;
 
 fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
-fun local_terminal_proof text int = Seq.THEN (proof (Some text), local_qed None int);
+fun local_terminal_proof text pr = Seq.THEN (proof (Some text), local_qed None pr);
 val local_immediate_proof = local_terminal_proof (Basic (K same));
 val local_default_proof = local_terminal_proof default_text;