src/HOL/Tools/SMT/z3_replay_methods.ML

 
 
 (* congruence *)
 
 fun ctac ctxt prems i st = st |> (
-  resolve_tac (@{thm refl} :: prems) i
+  resolve_tac ctxt (@{thm refl} :: prems) i
   ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i))
 
 fun cong_basic ctxt thms t =
   let val st = Thm.trivial (certify_prop ctxt t)
   in

   by fast+}
 
 fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
   Method.insert_tac thms
   THEN' (Classical.fast_tac ctxt'
-    ORELSE' dresolve_tac cong_dest_rules
+    ORELSE' dresolve_tac ctxt cong_dest_rules
     THEN' Classical.fast_tac ctxt'))
 
 fun cong ctxt thms = try_provers ctxt Z3_Proof.Monotonicity [
   ("basic", cong_basic ctxt thms),
   ("full", cong_full ctxt thms)] thms

   "(!!x. (~ P x) = Q x) ==> (~ (EX x. P x)) = (ALL x. Q x)"
   "(!!x. (~ P x) = Q x) ==> (~ (ALL x. P x)) = (EX x. Q x)"
   by fast+}
 
 fun quant_intro ctxt [thm] t =
-    prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac (thm :: quant_intro_rules))))
+    prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac ctxt (thm :: quant_intro_rules))))
   | quant_intro ctxt thms t = replay_rule_error ctxt Z3_Proof.Quant_Intro thms t
 
 
 (* distributivity of conjunctions and disjunctions *)