src/Pure/Isar/proof.ML
changeset 6683 b7293047b0f4
parent 6529 0f4c2ebc5018
child 6731 57e761134c85
     1.1 --- a/src/Pure/Isar/proof.ML	Fri May 21 11:38:23 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri May 21 11:38:57 1999 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4    val next_block: state -> state
     1.5    val end_block: state -> state
     1.6    val at_bottom: state -> bool
     1.7 -  val local_qed: (state -> state Seq.seq) -> state -> state Seq.seq
     1.8 +  val local_qed: (state -> state Seq.seq) -> bool -> state -> state Seq.seq
     1.9    val global_qed: (state -> state Seq.seq) -> bstring option
    1.10      -> theory attribute list option -> state -> theory * {kind: string, name: string, thm: thm}
    1.11  end;
    1.12 @@ -624,7 +624,7 @@
    1.13      |> opt_solve
    1.14    end;
    1.15  
    1.16 -fun local_qed finalize state =
    1.17 +fun local_qed finalize int state =	(* FIXME handle int *)
    1.18    state
    1.19    |> finish_proof false finalize
    1.20    |> (Seq.flat o Seq.map finish_local);