diff -r 9e35c1662aec -r d22294b20573 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Tools/atomize_elim.ML	Wed May 21 10:30:07 2025 +0200
@@ -54,7 +54,7 @@
 *)
 fun atomize_elim_conv ctxt ct =
     (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
-    then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems)
+    then_conv Raw_Simplifier.rewrite_wrt ctxt true (Named_Theorems.get ctxt named_theorems)
     then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))