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 =