--- 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
--- 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;