more precise scope of atomize

--- 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