--- 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);