src/Pure/Isar/code.ML

         val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
         val (vs'', _) = logical_typscheme thy (c, ty');
       in (c, (vs'', binder_types ty')) end;
     val c' :: cs' = map (analyze_constructor thy) cs;
     val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
-    val vs = Name.names Name.context Name.aT sorts;
+    val vs = Name.invent_names Name.context Name.aT sorts;
     val cs''' = map (inst vs) cs'';
   in (tyco, (vs, rev cs''')) end;
 
 fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
  of (_, entry) :: _ => SOME entry
   | _ => NONE;
 
 fun get_type thy tyco = case get_type_entry thy tyco
  of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
   | NONE => arity_number thy tyco
-      |> Name.invents Name.context Name.aT
+      |> Name.invent Name.context Name.aT
       |> map (rpair [])
       |> rpair []
       |> rpair false;
 
 fun get_abstype_spec thy tyco = case get_type_entry thy tyco

         fun tvars_of T = rev (Term.add_tvarsT T []);
         val vss = map (tvars_of o snd o head_eqn) thms;
         fun inter_sorts vs =
           fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
         val sorts = map_transpose inter_sorts vss;
-        val vts = Name.names Name.context Name.aT sorts;
+        val vts = Name.invent_names Name.context Name.aT sorts;
         val thms' =
           map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
         val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
         fun head_conv ct = if can Thm.dest_comb ct
           then Conv.fun_conv head_conv ct