--- a/src/HOL/Nominal/nominal_primrec.ML Sun Dec 01 14:24:10 2024 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Dec 01 18:12:24 2024 +0100
@@ -155,8 +155,8 @@
| SOME (ls, cargs', rs, rhs, eq) =>
let
val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
- val rargs = map fst recs;
- val subs = map (rpair dummyT o fst) (Term.variant_frees rhs rargs);
+ val rargs = map (rpair dummyT o fst o fst) recs;
+ val subs = Term.variant_frees rhs rargs;
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle RecError s => primrec_eq_err lthy s eq