src/HOL/Tools/SMT/z3_replay_methods.ML

 fun dest_prop (Const (@{const_name Trueprop}, _) $ t) = t
   | dest_prop t = t
 
 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 =
       (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of
         SOME thm => thm

     fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b)
   in Vartab.fold (cons o cert_inst) (sel inst) [] end
 
 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 =
   (case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of
     SOME thm => thm

     if eq_list (op aconv) (ls, rs) then SOME (ls, (HOLogic.mk_eq (lhs', rhs')))
     else NONE
   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
 
 fun focus_eq f ctxt t =