# HG changeset patch
# User wenzelm
# Date 1248633491 -7200
# Node ID 21d7b452439535c6f19f3d135851c314cb46374c
# Parent  752dbe71cc890c8d3f2ad6d3e55c4ceeb9f7bdce
replaced old METAHYPS by FOCUS;

diff -r 752dbe71cc89 -r 21d7b4524395 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 26 19:54:37 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 26 20:38:11 2009 +0200
@@ -3232,7 +3232,7 @@
 code_const approx' (Eval "Float'_Arith.approx'")
 
 ML {*
-  fun reorder_bounds_tac i prems =
+  fun reorder_bounds_tac prems i =
     let
       fun variable_of_bound (Const ("Trueprop", _) $
                              (Const (@{const_name "op :"}, _) $
@@ -3337,7 +3337,7 @@
       REPEAT (FIRST' [etac @{thm intervalE},
                       etac @{thm meta_eqE},
                       rtac @{thm impI}] i)
-      THEN METAHYPS (reorder_bounds_tac i) i
+      THEN 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
diff -r 752dbe71cc89 -r 21d7b4524395 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Jul 26 19:54:37 2009 +0200
+++ b/src/HOL/Tools/record.ML	Sun Jul 26 20:38:11 2009 +0200
@@ -2161,7 +2161,7 @@
       fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
         st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
         THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
-        THEN (METAHYPS equality_tac 1))
+        THEN (FOCUS (fn {prems, ...} => equality_tac prems) context 1))
              (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
       end);
      val equality = timeit_msg "record equality proof:" equality_prf;