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