diff -r f6c6d0988fba -r 39cd50407f79 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Aug 13 18:31:40 2024 +0200
+++ b/src/HOL/Tools/record.ML	Tue Aug 13 18:53:24 2024 +0200
@@ -1384,7 +1384,8 @@
           SOME (Goal.prove_sorry_global thy [] [] prop
             (fn {context = ctxt', ...} =>
               simp_tac (put_simpset (get_simpset thy) ctxt'
-                addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
+                addsimps @{thms simp_thms}
+                |> Simplifier.add_proc (split_simproc (K ~1))) 1))
         end handle TERM _ => NONE)
     | _ => NONE)
   end;
@@ -1466,7 +1467,7 @@
       | is_all _ = 0;
   in
     if has_rec goal then
-      full_simp_tac (put_simpset HOL_basic_ss ctxt addsimprocs [split_simproc is_all]) i
+      full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_proc (split_simproc is_all)) i
     else no_tac
   end);