1.1 --- a/src/HOL/HOL.thy	Tue Jul 03 15:23:11 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jul 03 17:17:04 2007 +0200
     1.3 @@ -1547,12 +1547,7 @@
     1.4  text {* Evaluation *}
     1.5  
     1.6  method_setup evaluation = {*
     1.7 -let
     1.8 -
     1.9 -fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
    1.10 -  (Conv.goals_conv (equal i) Codegen.evaluation_conv));
    1.11 -
    1.12 -in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
    1.13 +  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
    1.14  *} "solve goal by evaluation"
    1.15  
    1.16  
    1.17 @@ -1676,13 +1671,8 @@
    1.18  subsubsection {* Normalization by evaluation *}
    1.19  
    1.20  method_setup normalization = {*
    1.21 -let
    1.22 -  fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
    1.23 -    (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
    1.24 -      NBE.normalization_conv)));
    1.25 -in
    1.26 -  Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
    1.27 -end
    1.28 +  Method.no_args (Method.SIMPLE_METHOD'
    1.29 +    (CONVERSION (HOLogic.Trueprop_conv NBE.normalization_conv) THEN' resolve_tac [TrueI, refl]))
    1.30  *} "solve goal by normalization"
    1.31  
    1.32  

     2.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Tue Jul 03 15:23:11 2007 +0200
     2.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Jul 03 17:17:04 2007 +0200
     2.3 @@ -150,14 +150,14 @@
     2.4  let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
     2.5  in
     2.6    ObjectLogic.full_atomize_tac
     2.7 -  THEN_ALL_NEW eta_long_tac
     2.8 +  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
     2.9    THEN_ALL_NEW simp_tac ss
    2.10    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
    2.11    THEN_ALL_NEW ObjectLogic.full_atomize_tac
    2.12    THEN_ALL_NEW div_mod_tac ctxt
    2.13    THEN_ALL_NEW splits_tac ctxt
    2.14    THEN_ALL_NEW simp_tac ss
    2.15 -  THEN_ALL_NEW eta_long_tac
    2.16 +  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    2.17    THEN_ALL_NEW nat_to_int_tac ctxt
    2.18    THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
    2.19    THEN_ALL_NEW core_cooper_tac ctxt

     3.1 --- a/src/HOL/arith_data.ML	Tue Jul 03 15:23:11 2007 +0200
     3.2 +++ b/src/HOL/arith_data.ML	Tue Jul 03 17:17:04 2007 +0200
     3.3 @@ -898,9 +898,7 @@
     3.4        THEN (
     3.5          (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
     3.6            THEN_ALL_NEW
     3.7 -            ((fn j => PRIMITIVE
     3.8 -                        (Conv.fconv_rule
     3.9 -                          (Conv.goals_conv (equal j) (Drule.beta_eta_conversion))))
    3.10 +            (CONVERSION Drule.beta_eta_conversion
    3.11                THEN'
    3.12              (TRY o (etac notE THEN' eq_assume_tac)))
    3.13        ) i