diff -r d8fff0b94c53 -r cbc38731d42f src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 03 17:20:51 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 03 19:08:04 2015 +0100
@@ -3641,16 +3641,16 @@
                |> 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),
@@ -3663,9 +3663,9 @@
        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),