diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 21 10:30:34 2025 +0200
@@ -257,7 +257,7 @@
   Thm.forall_intr_vars #>
   Conv.fconv_rule (gen_normalize1_conv ctxt) #>
   (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
-  Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
+  Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
 
 fun gen_norm1_safe ctxt (i, thm) =
   (case try (gen_normalize1 ctxt) thm of