diff -r 8f0b2daa7eaa -r d93ead9ac6df src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Jun 12 12:44:47 2025 +0200
@@ -36,8 +36,8 @@
 val HOL_basic_ss' =
   simpset_of (put_simpset HOL_basic_ss \<^context>
     addsimps @{thms simp_thms prod.inject}
-    setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
-    setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
+    |> Simplifier.set_unsafe_solver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
+    |> Simplifier.set_unsafe_solver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
 
 
 (* auxillary functions *)