# HG changeset patch
# User haftmann
# Date 1590839315 0
# Node ID 435cdc77211019bbf5915aac7bf44c7916e0cc8e
# Parent  3956d85e8e817e2845e5979e1fe216bc604c7a6c
specific atomization inert to later rule set modifications

diff -r 3956d85e8e81 -r 435cdc772110 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sat May 30 11:48:28 2020 +0000
+++ b/src/FOL/simpdata.ML	Sat May 30 11:48:35 2020 +0000
@@ -80,6 +80,9 @@
   val iff_exI = @{thm iff_exI}
   val all_comm = @{thm all_comm}
   val ex_comm = @{thm ex_comm}
+  val atomize =
+    let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_iff atomize_conj}
+    in fn ctxt => Raw_Simplifier.rewrite ctxt true rules end
 );
 
 
diff -r 3956d85e8e81 -r 435cdc772110 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Sat May 30 11:48:28 2020 +0000
+++ b/src/HOL/Tools/simpdata.ML	Sat May 30 11:48:35 2020 +0000
@@ -33,6 +33,9 @@
   val iff_exI = @{thm iff_exI}
   val all_comm = @{thm all_comm}
   val ex_comm = @{thm ex_comm}
+  val atomize =
+    let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_conj}
+    in fn ctxt => Raw_Simplifier.rewrite ctxt true rules end
 );
 
 structure Simpdata =
diff -r 3956d85e8e81 -r 435cdc772110 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Sat May 30 11:48:28 2020 +0000
+++ b/src/Provers/quantifier1.ML	Sat May 30 11:48:35 2020 +0000
@@ -60,6 +60,7 @@
   val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
   val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
   val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
+  val atomize: Proof.context -> conv
 end;
 
 signature QUANTIFIER1 =
@@ -187,7 +188,7 @@
   fun prove_one_point_all_tac ctxt =
     EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
       resolve_tac ctxt [@{thm equal_allI}],
-      Object_Logic.full_atomize_tac ctxt,
+      CONVERSION (Data.atomize ctxt),
       resolve_tac ctxt [@{thm equal_intr_rule}],
       tac ctxt,
       tac ctxt];