# HG changeset patch
# User wenzelm
# Date 1704019805 -3600
# Node ID 6e6f76c5dd96933f6cba2b42c479f653e9940eaa
# Parent  0824ca1f1da02a42051d893e49451db56a703f68
tuned names (again);

diff -r 0824ca1f1da0 -r 6e6f76c5dd96 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 30 22:53:03 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 31 11:50:05 2023 +0100
@@ -1087,12 +1087,12 @@
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
 
         val types = present @ witnessed @ map (`Logic.dummy_tfree) extra';
-        fun get_type S = types |> get_first (fn (U, S') => if le (S', S) then SOME U else NONE);
+        fun get_type S = types |> get_first (fn (T', S') => if le (S', S) then SOME T' else NONE);
         fun map_atyp T =
           if Types.defined present_set T then raise Same.SAME
           else
             (case get_type (Type.sort_of_atyp T) of
-              SOME U => U
+              SOME T' => T'
             | NONE => raise Fail "strip_shyps: bad type variable in proof term");
         val map_ztyp =
           ZTypes.unsynchronized_cache