src/Provers/quantifier1.ML
changeset 72142 3956d85e8e81
parent 72112 4f4695757980
child 72143 435cdc772110
--- 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