diff -r 23957ebffaf7 -r ee680c69de38 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 21 19:26:09 2025 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Jan 21 19:26:39 2025 +0100
@@ -37,8 +37,8 @@
 
 val perm_bool = mk_meta_eq @{thm perm_bool_def};
 val perm_boolI = @{thm perm_boolI};
-val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
-  (Drule.strip_imp_concl (Thm.cprop_of perm_boolI))));
+val (_, [perm_boolI_pi, _]) = Drule.strip_comb (Thm.dest_arg
+  (Drule.strip_imp_concl (Thm.cprop_of perm_boolI)));
 
 fun mk_perm_bool ctxt pi th =
   th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;