--- a/src/HOL/Nominal/nominal_primrec.ML Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sat Nov 30 19:21:38 2024 +0100
@@ -156,8 +156,7 @@
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)
- (rev (Term.rename_wrt_term rhs rargs));
+ val subs = map (rpair dummyT o fst) (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