diff -r 8b477e3e15fa -r e23aab2df03c src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sun Jul 21 22:01:03 2024 +0200
+++ b/src/Pure/term_subst.ML	Sun Jul 21 22:34:25 2024 +0200
@@ -230,8 +230,10 @@
 (* zero var indexes *)
 
 fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
-  let val (x', used') = Name.variant_bound x used
-  in if x = x' andalso i = 0 then (inst, used') else (ins (v, mk ((x', 0), X)) inst, used') end;
+  let
+    val (x', used') = Name.variant_bound x used;
+    val inst' = if x = x' andalso i = 0 then inst else ins (v, mk ((x', 0), X)) inst;
+  in (inst', used') end;
 
 fun zero_var_indexes_inst used ts =
   let