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;