src/Pure/variable.ML
changeset 81521 1bfad73ab115
parent 81519 cdc43c0fdbfc
child 81543 fa37ee54644c
--- a/src/Pure/variable.ML	Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Pure/variable.ML	Sun Dec 01 14:01:47 2024 +0100
@@ -327,7 +327,7 @@
   | bounds =>
       let
         val names = Term.declare_term_names t (names_of ctxt);
-        val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names));
+        val xs = rev (Name.variants names (rev (map #2 bounds)));
         fun substs (((b, T), _), x') =
           let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U))
           in [subst T, subst (Type_Annotation.ignore_type T)] end;