--- a/src/HOL/HOL.thy Tue Jul 03 15:23:11 2007 +0200
+++ b/src/HOL/HOL.thy Tue Jul 03 17:17:04 2007 +0200
@@ -1547,12 +1547,7 @@
text {* Evaluation *}
method_setup evaluation = {*
-let
-
-fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
- (Conv.goals_conv (equal i) Codegen.evaluation_conv));
-
-in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
+ Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
*} "solve goal by evaluation"
@@ -1676,13 +1671,8 @@
subsubsection {* Normalization by evaluation *}
method_setup normalization = {*
-let
- fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
- (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
- NBE.normalization_conv)));
-in
- Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
-end
+ Method.no_args (Method.SIMPLE_METHOD'
+ (CONVERSION (HOLogic.Trueprop_conv NBE.normalization_conv) THEN' resolve_tac [TrueI, refl]))
*} "solve goal by normalization"
--- a/src/HOL/Tools/Qelim/presburger.ML Tue Jul 03 15:23:11 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML Tue Jul 03 17:17:04 2007 +0200
@@ -150,14 +150,14 @@
let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
in
ObjectLogic.full_atomize_tac
- THEN_ALL_NEW eta_long_tac
+ THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW simp_tac ss
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
THEN_ALL_NEW ObjectLogic.full_atomize_tac
THEN_ALL_NEW div_mod_tac ctxt
THEN_ALL_NEW splits_tac ctxt
THEN_ALL_NEW simp_tac ss
- THEN_ALL_NEW eta_long_tac
+ THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW nat_to_int_tac ctxt
THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
THEN_ALL_NEW core_cooper_tac ctxt
--- a/src/HOL/arith_data.ML Tue Jul 03 15:23:11 2007 +0200
+++ b/src/HOL/arith_data.ML Tue Jul 03 17:17:04 2007 +0200
@@ -898,9 +898,7 @@
THEN (
(TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
THEN_ALL_NEW
- ((fn j => PRIMITIVE
- (Conv.fconv_rule
- (Conv.goals_conv (equal j) (Drule.beta_eta_conversion))))
+ (CONVERSION Drule.beta_eta_conversion
THEN'
(TRY o (etac notE THEN' eq_assume_tac)))
) i