src/HOL/Decision_Procs/approximation.ML

     val m = map (fn (name, _) => (name, @{typ real})) (Term.add_tvars t [])
     val t = Term.subst_TVars m t
   in t end
 
 fun apply_tactic ctxt term tactic =
-  cterm_of (Proof_Context.theory_of ctxt) term
+  Proof_Context.cterm_of ctxt term
   |> Goal.init
   |> SINGLE tactic
   |> the |> prems_of |> hd
 
 fun prepare_form ctxt term = apply_tactic ctxt term (

          |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
          |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
          |> foldr1 HOLogic.mk_conj))
 
 fun approx_arith prec ctxt t = realify t
-     |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+     |> Proof_Context.cterm_of ctxt
      |> Reification.conv ctxt form_equations
      |> prop_of
      |> Logic.dest_equals |> snd
      |> dest_interpret |> fst
      |> mk_approx' prec