| changeset 81517 | 1b33a7a3c80c |
| parent 81512 | c1aa8a61ee65 |
| child 81518 | f012cbfd96d0 |
--- a/src/Pure/variable.ML Sat Nov 30 19:21:38 2024 +0100 +++ b/src/Pure/variable.ML Sat Nov 30 21:01:59 2024 +0100 @@ -278,10 +278,7 @@ (* renaming term/type frees *) fun variant_frees ctxt ts frees = - let - val names = names_of (fold declare_names ts ctxt); - val xs = fst (fold_map Name.variant (map #1 frees) names); - in xs ~~ map snd frees end; + Name.variant_names (names_of (fold declare_names ts ctxt)) frees;