# HG changeset patch
# User wenzelm
# Date 1701872114 -3600
# Node ID bfe5c20074e48aee7fc9588a0a6919a35c62b97a
# Parent  feb94ac5df414fc757e8a8573df3dbd8a1622155
proper substitution of types within term;

diff -r feb94ac5df41 -r bfe5c20074e4 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Dec 06 13:16:34 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 15:15:14 2023 +0100
@@ -523,10 +523,9 @@
           if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S)
           else raise Same.SAME);
     val term =
-      if Names.is_empty frees then Same.same else
-        subst_term_same typ (fn ((x, i), T) =>
-          if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
-          else raise Same.SAME);
+      subst_term_same typ (fn ((x, i), T) =>
+        if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
+        else raise Same.SAME);
   in Same.commit (map_proof_same typ term) prf end;
 
 fun varifyT_proof names prf =