--- a/src/Pure/type.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Pure/type.ML Sun Dec 01 14:01:47 2024 +0100
@@ -346,7 +346,7 @@
build (t |> (Term.fold_types o Term.fold_atyps)
(fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
val used = Name.build_context (t |> Term.declare_tvar_names (K true));
- val ys = #1 (fold_map Name.variant (map #1 xs) used);
+ val ys = Name.variants used (map #1 xs);
in map2 (fn (a, S) => fn b => ((a, S), ((b, 0), S))) xs ys end;
fun varify_global fixed t =