# HG changeset patch
# User wenzelm
# Date 1183475824 -7200
# Node ID 438c5d2db4828891e376de60a30738f5b9bd00af
# Parent  958f9d9cfb63530ce143a3531a90fe00c36be992
CONVERSION tactical;

diff -r 958f9d9cfb63 -r 438c5d2db482 src/HOL/HOL.thy
--- 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"
 
 
diff -r 958f9d9cfb63 -r 438c5d2db482 src/HOL/Tools/Qelim/presburger.ML
--- 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
diff -r 958f9d9cfb63 -r 438c5d2db482 src/HOL/arith_data.ML
--- 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