--- a/src/HOL/Tools/SMT/smtlib_isar.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML	Wed May 21 10:30:34 2025 +0200
@@ -43,7 +43,7 @@
 
 fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
   let val thy = Proof_Context.theory_of ctxt in
-    Raw_Simplifier.rewrite_term thy rewrite_rules []
+    Simplifier.rewrite_term thy rewrite_rules []
     #> Object_Logic.atomize_term ctxt
     #> not (null ll_defs) ? unlift_term ll_defs
     #> simplify_bool