--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Mar 03 19:08:04 2015 +0100
@@ -88,7 +88,7 @@
fun dest_thm thm = dest_prop (Thm.concl_of thm)
-fun certify_prop ctxt t = SMT_Util.certify ctxt (as_prop t)
+fun certify_prop ctxt t = Proof_Context.cterm_of ctxt (as_prop t)
fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
| try_provers ctxt rule ((name, prover) :: named_provers) thms t =
@@ -108,13 +108,13 @@
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt)
+ let val certT = Proof_Context.ctyp_of ctxt
in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
else thm
fun match_instantiate ctxt t thm =
let
- val cert = SMT_Util.certify ctxt
+ val cert = Proof_Context.cterm_of ctxt
val thm' = match_instantiateT ctxt t thm
in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
@@ -402,7 +402,7 @@
end
fun forall_intr ctxt t thm =
- let val ct = Thm.cterm_of (Proof_Context.theory_of ctxt) t
+ let val ct = Proof_Context.cterm_of ctxt t
in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end
in