Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_primrec.ML
changeset 81541 5335b1ca6233
parent 81523 06eebdc93ea8 
--- a/src/HOL/Nominal/nominal_primrec.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -156,7 +156,7 @@
             let
               val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
               val rargs = map (rpair dummyT o fst o fst) recs;
-              val subs = Term.variant_frees rhs rargs;
+              val subs = Term.variant_bounds 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
isabelle