diff -r cbc38731d42f -r 0fbed69ff081 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -3597,11 +3597,11 @@
         | variable_of_bound t = raise TERM ("variable_of_bound", [t])
 
       val variable_bounds
-        = map (` (variable_of_bound o prop_of)) prems
+        = map (`(variable_of_bound o Thm.prop_of)) prems
 
       fun add_deps (name, bnds)
         = Graph.add_deps_acyclic (name,
-            remove (op =) name (Term.add_free_names (prop_of bnds) []))
+            remove (op =) name (Term.add_free_names (Thm.prop_of bnds) []))
 
       val order = Graph.empty
                   |> fold Graph.new_node variable_bounds
@@ -3634,7 +3634,7 @@
         = case AList.lookup (op =) splitting name
           of SOME s => HOLogic.mk_number @{typ nat} s
            | NONE => @{term "0 :: nat"}
-      val vs = nth (prems_of st) (i - 1)
+      val vs = nth (Thm.prems_of st) (i - 1)
                |> Logic.strip_imp_concl
                |> HOLogic.dest_Trueprop
                |> Term.strip_comb |> snd |> List.last
@@ -3659,7 +3659,9 @@
           THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
        end
 
-     | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
+     | SOME t =>
+       if length vs <> 1
+       then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st]))
        else let
          val t = t
               |> HOLogic.mk_number @{typ nat}