# HG changeset patch
# User wenzelm
# Date 1634550057 -7200
# Node ID f07761ee5a7ffc392bae860d617ce21e0853cf2c
# Parent  45c09620f726c0bd483a9e5082153c49938aa69a
more robust Variable.revert_bounds (see also b12f2cef3ee5);

diff -r 45c09620f726 -r f07761ee5a7f src/Pure/variable.ML
--- 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);