src/Pure/variable.ML

     [] => t
   | 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));
-        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);
 
 
 
 (** fixes **)