diff -r 6f3771c00280 -r 47d138cae708 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 31 09:30:32 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 31 09:30:32 2013 +0200
@@ -3533,7 +3533,7 @@
                       rtac @{thm impI}] i)
       THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
       THEN DETERM (TRY (filter_prems_tac (K false) i))
-      THEN DETERM (Reflection.gen_reify_tac ctxt form_equations NONE i)
+      THEN DETERM (Reflection.reify_tac ctxt form_equations NONE i)
       THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
       THEN gen_eval_tac (approximation_conv ctxt) ctxt i))
  *} "real number approximation"
@@ -3633,7 +3633,7 @@
       THEN DETERM (TRY (filter_prems_tac (K false) 1)))
 
   fun reify_form ctxt term = apply_tactic ctxt term
-     (Reflection.gen_reify_tac ctxt form_equations NONE 1)
+     (Reflection.reify_tac ctxt form_equations NONE 1)
 
   fun approx_form prec ctxt t =
           realify t
@@ -3650,7 +3650,7 @@
            |> foldr1 HOLogic.mk_conj))
 
   fun approx_arith prec ctxt t = realify t
-       |> Reflection.gen_reify ctxt form_equations
+       |> Reflection.reify ctxt form_equations
        |> prop_of
        |> HOLogic.dest_Trueprop
        |> HOLogic.dest_eq |> snd