diff -r 31b05aef022d -r 1b33a7a3c80c src/Pure/variable.ML
--- 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;