--- a/src/Pure/Isar/element.ML Mon Mar 21 11:54:45 2016 +0100
+++ b/src/Pure/Isar/element.ML Mon Mar 21 19:57:56 2016 +0100
@@ -40,10 +40,9 @@
val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) ->
term list list -> term list -> Proof.context -> Proof.state
val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
- string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
+ string -> term list list -> Proof.context -> Proof.state -> Proof.state
val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
- string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
- Proof.state
+ string -> term list list -> term list -> Proof.context -> Proof.state -> Proof.state
val transform_witness: morphism -> witness -> witness
val conclude_witness: Proof.context -> witness -> thm
val pretty_witness: Proof.context -> witness -> Pretty.T
@@ -285,7 +284,7 @@
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness end;
-fun proof_local cmd goal_ctxt int after_qed propp =
+fun proof_local cmd goal_ctxt after_qed propp =
let
fun after_qed' (result_ctxt, results) state' =
after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state';
@@ -303,12 +302,12 @@
val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
-fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
- gen_witness_proof (proof_local cmd goal_ctxt int)
+fun witness_local_proof after_qed cmd wit_propss goal_ctxt =
+ gen_witness_proof (proof_local cmd goal_ctxt)
(fn wits => fn _ => after_qed wits) wit_propss [];
-fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
- gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
+fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt =
+ gen_witness_proof (proof_local cmd goal_ctxt) after_qed wit_propss eq_props;
end;