--- a/src/HOL/Decision_Procs/Approximation.thy Thu Jul 30 11:23:57 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jul 30 12:20:43 2009 +0200
@@ -3337,7 +3337,7 @@
REPEAT (FIRST' [etac @{thm intervalE},
etac @{thm meta_eqE},
rtac @{thm impI}] i)
- THEN FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+ THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
THEN TRY (filter_prems_tac (K false) i)
THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i