diff -r 10d731b06ed7 -r 84472e198515 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jun 09 20:22:22 2011 +0200
@@ -149,7 +149,7 @@
     fun print_def name (vs, ty) [] =
           let
             val (tys, ty') = Code_Thingol.unfold_fun ty;
-            val params = Name.invents (snd reserved) "a" (length tys);
+            val params = Name.invent (snd reserved) "a" (length tys);
             val tyvars = intro_tyvars vs reserved;
             val vars = intro_vars params reserved;
           in
@@ -214,7 +214,7 @@
                     (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
                     (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
                       ["final", "case", "class", deresolve co]) vs_args)
-                    (Name.names (snd reserved) "a" tys),
+                    (Name.invent_names (snd reserved) "a" tys),
                     str "extends",
                     applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
                       ((str o deresolve) name) vs
@@ -238,9 +238,9 @@
             fun print_classparam_def (classparam, ty) =
               let
                 val (tys, ty) = Code_Thingol.unfold_fun ty;
-                val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
+                val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1;
                 val proto_vars = intro_vars [implicit_name] reserved;
-                val auxs = Name.invents (snd proto_vars) "a" (length tys);
+                val auxs = Name.invent (snd proto_vars) "a" (length tys);
                 val vars = intro_vars auxs proto_vars;
               in
                 concat [str "def", constraint (Pretty.block [applify "(" ")"
@@ -267,7 +267,7 @@
             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
               let
-                val aux_tys = Name.names (snd reserved) "a" tys;
+                val aux_tys = Name.invent_names (snd reserved) "a" tys;
                 val auxs = map fst aux_tys;
                 val vars = intro_vars auxs reserved;
                 val aux_abstr = if null auxs then [] else [enum "," "(" ")"