# HG changeset patch
# User wenzelm
# Date 1183658486 -7200
# Node ID ad95084a5c63b6c9f0dd3c2b1fee030dea7bc9ac
# Parent  aaba731fce8655c2c898e8ea0fc290a77020b3a3
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;

diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Complex/ex/linrtac.ML
--- a/src/HOL/Complex/ex/linrtac.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -73,7 +73,7 @@
 
 
 fun linr_tac ctxt q i = 
-    (ObjectLogic.atomize_tac i) 
+    (ObjectLogic.atomize_prems_tac i) 
 	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i))
 	THEN (fn st =>
   let
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Complex/ex/mirtac.ML
--- a/src/HOL/Complex/ex/mirtac.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -81,7 +81,7 @@
 
 
 fun mir_tac ctxt q i = 
-    (ObjectLogic.atomize_tac i)
+    (ObjectLogic.atomize_prems_tac i)
 	THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
 	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
 	THEN (fn st =>
@@ -161,4 +161,4 @@
      "decision procedure for MIR arithmetic");
 
 
-end
\ No newline at end of file
+end
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -1083,7 +1083,7 @@
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn prems => EVERY
         [rtac indrule_lemma' 1,
-         (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+         (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms' 1),
             simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -215,7 +215,7 @@
         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
           (map cert insts)) induct;
         val (tac, _) = Library.foldl mk_unique_tac
-          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
+          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
               THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
             descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
 
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -122,7 +122,7 @@
       (fn prems =>
          [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
           rtac (cterm_instantiate inst induction) 1,
-          ALLGOALS ObjectLogic.atomize_tac,
+          ALLGOALS ObjectLogic.atomize_prems_tac,
           rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -403,7 +403,7 @@
 
         val inj_thm = Goal.prove_global thy5 [] []
           (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
-            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
              REPEAT (EVERY
                [rtac allI 1, rtac impI 1,
                 exh_tac (exh_thm_of dt_info) 1,
@@ -429,7 +429,7 @@
         val elem_thm = 
             Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
               (fn _ =>
-               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
                 rewrite_goals_tac rewrites,
                 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
                   ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
@@ -465,7 +465,7 @@
     val iso_thms = if length descr = 1 then [] else
       Library.drop (length newTs, split_conj_thm
         (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
-           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
             rewrite_goals_tac (mk_meta_eq choice_eq ::
               symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
@@ -606,7 +606,7 @@
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn prems => EVERY
         [rtac indrule_lemma' 1,
-         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
+         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -388,7 +388,7 @@
           [rtac (#raw_induct ind_info) 1,
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
-             [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
+             [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
           (NameSpace.qualified qualifier "induct" :: vs @ Ps @
@@ -449,7 +449,7 @@
            etac elimR 1,
            ALLGOALS (asm_simp_tac HOL_basic_ss),
            rewrite_goals_tac rews,
-           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
+           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
           (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -556,7 +556,7 @@
   Function mkcl converts theorems to clauses.*)
 fun MESON mkcl cltac i st = 
   SELECT_GOAL
-    (EVERY [ObjectLogic.atomize_tac 1,
+    (EVERY [ObjectLogic.atomize_prems_tac 1,
             rtac ccontr 1,
 	    METAHYPS (fn negs =>
 		      EVERY1 [skolemize_prems_tac negs,
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Tools/res_atp_methods.ML
--- a/src/HOL/Tools/res_atp_methods.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -9,7 +9,7 @@
   
 (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
 fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
-    (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
+    (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac,
 		  METAHYPS(fn negs =>
 			      HEADGOAL(Tactic.rtac 
 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -428,7 +428,7 @@
 
 val pre_cnf_tac =
         rtac ccontr THEN'
-        ObjectLogic.atomize_tac THEN'
+        ObjectLogic.atomize_prems_tac THEN'
         CONVERSION Drule.beta_eta_conversion;
 
 (* ------------------------------------------------------------------------- *)
diff -r aaba731fce86 -r ad95084a5c63 src/HOL/ex/coopertac.ML
--- a/src/HOL/ex/coopertac.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/HOL/ex/coopertac.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -65,7 +65,7 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 
-fun linz_tac ctxt q i = ObjectLogic.atomize_tac i THEN (fn st =>
+fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
     val thy = ProofContext.theory_of ctxt
@@ -140,4 +140,4 @@
      linz_args linz_method,
      "decision procedure for linear integer arithmetic");
 
-end
\ No newline at end of file
+end
diff -r aaba731fce86 -r ad95084a5c63 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -196,7 +196,7 @@
 
 (* atomize rule statements *)
 
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
+fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
   | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
 
 
@@ -525,7 +525,7 @@
   bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
     (fn n => fn prems => fn ctxt => METHOD (fn facts =>
       HEADGOAL (insert_tac (prems @ facts) THEN'
-      ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)));
+      ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
 
 end;