--- a/src/Pure/variable.ML Sun Oct 17 19:46:01 2021 +0200
+++ b/src/Pure/variable.ML Mon Oct 18 11:40:57 2021 +0200
@@ -334,8 +334,10 @@
let
val names = Term.declare_term_names t (names_of ctxt);
val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names));
- fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
- in Term.subst_atomic (map2 subst bounds xs) t end);
+ 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;
+ in Term.subst_atomic (maps substs (bounds ~~ xs)) t end);