diff -r d3328c562307 -r d769a183d51d src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Tools/record.ML	Sat Oct 21 21:19:02 2023 +0200
@@ -1322,8 +1322,9 @@
     P t = ~1: completely split
     P t > 0: split up to given bound of record extensions.*)
 fun split_simproc P =
-  Simplifier.make_simproc \<^context> "record_split"
-   {lhss = [\<^term>\<open>x::'a::{}\<close>],
+  Simplifier.make_simproc \<^context>
+   {name = "record_split",
+    lhss = [\<^term>\<open>x::'a::{}\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1348,7 +1349,8 @@
                   else NONE
                 end)
           else NONE
-      | _ => NONE)};
+      | _ => NONE),
+    identifier = []};
 
 fun ex_sel_eq_proc ctxt ct =
   let