replaced old METAHYPS by FOCUS;
authorwenzelm
Sun Jul 26 20:38:11 2009 +0200 (2009-07-26)
changeset 3221221d7b4524395
parent 32211 752dbe71cc89
child 32213 f1b166317ae2
replaced old METAHYPS by FOCUS;
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 26 19:54:37 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 26 20:38:11 2009 +0200
     1.3 @@ -3232,7 +3232,7 @@
     1.4  code_const approx' (Eval "Float'_Arith.approx'")
     1.5  
     1.6  ML {*
     1.7 -  fun reorder_bounds_tac i prems =
     1.8 +  fun reorder_bounds_tac prems i =
     1.9      let
    1.10        fun variable_of_bound (Const ("Trueprop", _) $
    1.11                               (Const (@{const_name "op :"}, _) $
    1.12 @@ -3337,7 +3337,7 @@
    1.13        REPEAT (FIRST' [etac @{thm intervalE},
    1.14                        etac @{thm meta_eqE},
    1.15                        rtac @{thm impI}] i)
    1.16 -      THEN METAHYPS (reorder_bounds_tac i) i
    1.17 +      THEN FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
    1.18        THEN TRY (filter_prems_tac (K false) i)
    1.19        THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
    1.20        THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
     2.1 --- a/src/HOL/Tools/record.ML	Sun Jul 26 19:54:37 2009 +0200
     2.2 +++ b/src/HOL/Tools/record.ML	Sun Jul 26 20:38:11 2009 +0200
     2.3 @@ -2161,7 +2161,7 @@
     2.4        fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
     2.5          st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
     2.6          THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
     2.7 -        THEN (METAHYPS equality_tac 1))
     2.8 +        THEN (FOCUS (fn {prems, ...} => equality_tac prems) context 1))
     2.9               (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
    2.10        end);
    2.11       val equality = timeit_msg "record equality proof:" equality_prf;