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