diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -157,7 +157,9 @@
   let
     val ctxt = Proof_Context.init_global thy
     val inline_defs = Named_Theorems.get ctxt \<^named_theorems>\<open>code_pred_inline\<close>
-    val th' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs) th
+    val th' =
+      Simplifier.full_simplify
+        (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps inline_defs) th
     (*val _ = print_step options
       ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
        ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))