src/Pure/term_subst.ML
changeset 80599 f8c070249502
parent 79409 e1895596e1b9
child 80607 e23aab2df03c
--- a/src/Pure/term_subst.ML	Sat Jul 20 19:30:03 2024 +0200
+++ b/src/Pure/term_subst.ML	Sat Jul 20 21:17:22 2024 +0200
@@ -230,7 +230,7 @@
 (* zero var indexes *)
 
 fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
-  let val (x', used') = Name.variant (if Name.is_bound x then "u" else x) 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;
 
 fun zero_var_indexes_inst used ts =