# HG changeset patch
# User wenzelm
# Date 1635176449 -7200
# Node ID 9bfbb5f7ec99ea9645c6e309457f94c5ac37a0d2
# Parent  d4829a7333e221812d2f4ee3fbd0399307a43f85
tuned;

diff -r d4829a7333e2 -r 9bfbb5f7ec99 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Mon Oct 25 17:37:24 2021 +0200
+++ b/src/Pure/term_subst.ML	Mon Oct 25 17:40:49 2021 +0200
@@ -108,7 +108,7 @@
       fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
         | subst (TFree v) =
             (case TFrees.lookup instT v of
-              SOME T => T
+              SOME T' => T'
             | NONE => raise Same.SAME)
         | subst _ = raise Same.SAME;
     in subst ty end;
@@ -122,7 +122,7 @@
         | subst (Free (x, T)) =
             let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
               (case Frees.lookup inst (x, T') of
-                 SOME t => t
+                 SOME t' => t'
                | NONE => if same then raise Same.SAME else Free (x, T'))
             end
         | subst (Var (xi, T)) = Var (xi, substT T)
@@ -151,7 +151,7 @@
     fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
       | subst_typ (TVar ((a, i), S)) =
           (case TVars.lookup instT ((a, i), S) of
-            SOME (T, j) => (maxify j; T)
+            SOME (T', j) => (maxify j; T')
           | NONE => (maxify i; raise Same.SAME))
       | subst_typ _ = raise Same.SAME
     and subst_typs (T :: Ts) =
@@ -170,7 +170,7 @@
       | subst (Var ((x, i), T)) =
           let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
             (case Vars.lookup inst ((x, i), T') of
-               SOME (t, j) => (maxify j; t)
+               SOME (t', j) => (maxify j; t')
              | NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
           end
       | subst (Bound _) = raise Same.SAME
@@ -193,7 +193,7 @@
         Var ((x, i), T) =>
           let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
             (case Vars.lookup inst ((x, i), T') of
-              SOME (u, j) => (maxify j; SOME u)
+              SOME (t', j) => (maxify j; SOME t')
             | NONE => (maxify i; if same then NONE else SOME (Var ((x, i), T'))))
           end
       | _ => NONE);