--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Mar 06 15:58:56 2015 +0100
@@ -88,7 +88,7 @@
fun dest_thm thm = dest_prop (Thm.concl_of thm)
-fun certify_prop ctxt t = Proof_Context.cterm_of ctxt (as_prop t)
+fun certify_prop ctxt t = Thm.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,12 +108,12 @@
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- Thm.instantiate (gen_certify_inst fst TVar (Proof_Context.ctyp_of ctxt) ctxt thm t, []) thm
+ Thm.instantiate (gen_certify_inst fst TVar (Thm.ctyp_of ctxt) ctxt thm t, []) thm
else thm
fun match_instantiate ctxt t thm =
let val thm' = match_instantiateT ctxt t thm in
- Thm.instantiate ([], gen_certify_inst snd Var (Proof_Context.cterm_of ctxt) ctxt thm' t) thm'
+ Thm.instantiate ([], gen_certify_inst snd Var (Thm.cterm_of ctxt) ctxt thm' t) thm'
end
fun apply_rule ctxt t =
@@ -400,7 +400,7 @@
end
fun forall_intr ctxt t thm =
- let val ct = Proof_Context.cterm_of ctxt t
+ let val ct = Thm.cterm_of ctxt t
in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end
in