tuned names (again);

--- 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