# HG changeset patch
# User haftmann
# Date 1590839308 0
# Node ID 3956d85e8e817e2845e5979e1fe216bc604c7a6c
# Parent  3867734b9a40f0bee9b0d24e9f526f1b68f6601c
more precise scope of atomize

diff -r 3867734b9a40 -r 3956d85e8e81 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Sat May 30 08:50:18 2020 +0000
+++ b/src/Provers/quantifier1.ML	Sat May 30 11:48:28 2020 +0000
@@ -187,10 +187,9 @@
   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,
       resolve_tac ctxt [@{thm equal_intr_rule}],
-      Object_Logic.atomize_prems_tac ctxt,
       tac ctxt,
-      Object_Logic.atomize_prems_tac ctxt,
       tac ctxt];
 end