--- a/src/HOL/Nominal/nominal_inductive.ML Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Aug 04 17:39:47 2024 +0200
@@ -46,7 +46,7 @@
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))
+ if member (op =) names (the_default "" (try (dest_Const_name o head_of) t))
then SOME perm_bool else NONE
| _ => NONE),
identifier = []};