src/HOL/Decision_Procs/Approximation.thy

                |> HOLogic.dest_Trueprop
                |> Term.strip_comb |> snd |> List.last
                |> HOLogic.dest_list
       val p = prec
               |> HOLogic.mk_number @{typ nat}
-              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+              |> Proof_Context.cterm_of ctxt
     in case taylor
     of NONE => let
          val n = vs |> length
                  |> HOLogic.mk_number @{typ nat}
-                 |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+                 |> Proof_Context.cterm_of ctxt
          val s = vs
                  |> map lookup_splitting
                  |> HOLogic.mk_list @{typ nat}
-                 |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+                 |> Proof_Context.cterm_of ctxt
        in
          (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
                                      (@{cpat "?prec::nat"}, p),
                                      (@{cpat "?ss::nat list"}, s)])
               @{thm "approx_form"}) i

 
      | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
        else let
          val t = t
               |> HOLogic.mk_number @{typ nat}
-              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+              |> Proof_Context.cterm_of ctxt
          val s = vs |> map lookup_splitting |> hd
-              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+              |> Proof_Context.cterm_of ctxt
        in
          rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
                                      (@{cpat "?t::nat"}, t),
                                      (@{cpat "?prec::nat"}, p)])
               @{thm "approx_tse_form"}) i st