tuned;

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

--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Dec 01 14:24:10 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Dec 01 18:12:24 2024 +0100
@@ -148,8 +148,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 PrimrecError (s, NONE) => primrec_error_eqn s eq