src/HOL/Tools/simpdata.ML
changeset 82641 d22294b20573
parent 71916 435cdc772110
child 82643 f1c14af17591
--- a/src/HOL/Tools/simpdata.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed May 21 10:30:07 2025 +0200
@@ -35,7 +35,7 @@
   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
+    in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end
 );
 
 structure Simpdata =