local_qed: obtain interactive flag;

--- a/src/Pure/Isar/method.ML	Fri May 21 11:38:23 1999 +0200
+++ b/src/Pure/Isar/method.ML	Fri May 21 11:38:57 1999 +0200
@@ -55,10 +55,10 @@
   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 -> Proof.state -> Proof.state Seq.seq
-  val local_terminal_proof: text -> Proof.state -> Proof.state Seq.seq
-  val local_immediate_proof: Proof.state -> Proof.state Seq.seq
-  val local_default_proof: 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 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 +301,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 = Seq.THEN (proof (Some text), local_qed None);
+fun local_terminal_proof text int = Seq.THEN (proof (Some text), local_qed None int);
 val local_immediate_proof = local_terminal_proof (Basic (K same));
 val local_default_proof = local_terminal_proof default_text;
 

--- a/src/Pure/Isar/proof.ML	Fri May 21 11:38:23 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Fri May 21 11:38:57 1999 +0200
@@ -58,7 +58,7 @@
   val next_block: state -> state
   val end_block: state -> state
   val at_bottom: state -> bool
-  val local_qed: (state -> state Seq.seq) -> state -> state Seq.seq
+  val local_qed: (state -> state Seq.seq) -> bool -> state -> state Seq.seq
   val global_qed: (state -> state Seq.seq) -> bstring option
     -> theory attribute list option -> state -> theory * {kind: string, name: string, thm: thm}
 end;
@@ -624,7 +624,7 @@
     |> opt_solve
   end;
 
-fun local_qed finalize state =
+fun local_qed finalize int state =	(* FIXME handle int *)
   state
   |> finish_proof false finalize
   |> (Seq.flat o Seq.map finish_local);