src/Pure/term_subst.ML

 (* zero var indexes *)
 
 fun zero_var_inst vars =
   fold (fn v as ((x, i), X) => fn (inst, used) =>
     let
-      val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
+      val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
     in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
   vars ([], Name.context) |> #1;
 
 fun zero_var_indexes_inst ts =
   let