--- a/src/HOL/Decision_Procs/Approximation.thy Sat Apr 20 20:57:49 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Apr 21 10:41:18 2013 +0200
@@ -3533,7 +3533,7 @@
rtac @{thm impI}] i)
THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
THEN DETERM (TRY (filter_prems_tac (K false) i))
- THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
+ THEN DETERM (Reflection.gen_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"
@@ -3632,7 +3632,7 @@
THEN DETERM (TRY (filter_prems_tac (K false) 1)))
fun reify_form context term = apply_tactic context term
- (Reflection.genreify_tac @{context} form_equations NONE 1)
+ (Reflection.gen_reify_tac @{context} 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.genreif ctxt form_equations
+ |> Reflection.gen_reify ctxt form_equations
|> prop_of
|> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> snd