src/Tools/Code/code_thingol.ML

         val (vs_tys, t') = unfold_abs_eta tys t;
       in (v_ty :: vs_tys, t') end
   | unfold_abs_eta tys t =
       let
         val ctxt = fold_varnames Name.declare t Name.context;
-        val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
+        val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
       in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
 
 fun eta_expand k (c as (name, (_, tys)), ts) =
   let
     val j = length ts;
     val l = k - j;
     val _ = if l > length tys
       then error ("Impossible eta-expansion for constant " ^ quote name) else ();
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
     val vs_tys = (map o apfst) SOME
-      (Name.names ctxt "a" ((take l o drop j) tys));
+      (Name.invent_names ctxt "a" ((take l o drop j) tys));
   in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
 
 fun contains_dict_var t =
   let
     fun cont_dict (Dict (_, d)) = cont_plain_dict d

     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val these_classparams = these o try (#params o AxClass.get_info thy);
     val classparams = these_classparams class;
     val further_classparams = maps these_classparams
       ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
-    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
+    val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
     val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
       Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
     val arity_typ = Type (tyco, map TFree vs);
     val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');

   if length ts < num_args then
     let
       val k = length ts;
       val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
       val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
-      val vs = Name.names ctxt "a" tys;
+      val vs = Name.invent_names ctxt "a" tys;
     in
       fold_map (translate_typ thy algbr eqngr permissive) tys
       ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
       #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
     end