--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Tue Feb 10 14:48:26 2015 +0100
@@ -636,10 +636,10 @@
fun skolemize vars =
apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
-fun discharge_sk_tac i st = (
+fun discharge_sk_tac ctxt i st = (
rtac @{thm trans} i
- THEN resolve_tac sk_rules i
- THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+ THEN resolve_tac ctxt sk_rules i
+ THEN (rtac @{thm refl} ORELSE' discharge_sk_tac ctxt) (i+1)
THEN rtac @{thm refl} i) st
end
@@ -847,13 +847,13 @@
fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
@{thm reflexive}, Old_Z3_Proof_Literals.true_thm]
- fun discharge_assms_tac rules =
- REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
+ fun discharge_assms_tac ctxt rules =
+ REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt)))
fun discharge_assms ctxt rules thm =
if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
else
- (case Seq.pull (discharge_assms_tac rules thm) of
+ (case Seq.pull (discharge_assms_tac ctxt rules thm) of
SOME (thm', _) => Goal.norm_result ctxt thm'
| NONE => raise THM ("failed to discharge premise", 1, [thm]))