src/Pure/Isar/code.ML

--- a/src/Pure/Isar/code.ML	Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/Isar/code.ML	Thu Jun 09 20:22:22 2011 +0200
@@ -433,7 +433,7 @@
       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;
 
@@ -444,7 +444,7 @@
 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;
@@ -779,7 +779,7 @@
         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'))));