diff -r d3328c562307 -r d769a183d51d src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Oct 21 21:19:02 2023 +0200
@@ -44,14 +44,16 @@
   th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
 
 fun mk_perm_bool_simproc names =
-  Simplifier.make_simproc \<^context> "perm_bool"
-   {lhss = [\<^term>\<open>perm pi x\<close>],
+  Simplifier.make_simproc \<^context>
+   {name = "perm_bool",
+    lhss = [\<^term>\<open>perm pi x\<close>],
     proc = fn _ => fn _ => fn ct =>
       (case Thm.term_of ct of
         Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ t =>
           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
-       | _ => NONE)};
+       | _ => NONE),
+    identifier = []};
 
 fun transp ([] :: _) = []
   | transp xs = map hd xs :: transp (map tl xs);