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 =