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