1.1 --- a/src/Pure/axclass.ML	Wed Jun 08 22:16:21 2011 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Jun 09 20:22:22 2011 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4        |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
     1.5              c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
     1.6  
     1.7 -    val names = Name.invents Name.context Name.aT (length Ss);
     1.8 +    val names = Name.invent Name.context Name.aT (length Ss);
     1.9      val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
    1.10  
    1.11      val completions = super_class_completions |> map (fn c1 =>
    1.12 @@ -445,7 +445,7 @@
    1.13      val (th', thy') = Global_Theory.store_thm
    1.14        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
    1.15  
    1.16 -    val args = Name.names Name.context Name.aT Ss;
    1.17 +    val args = Name.invent_names Name.context Name.aT Ss;
    1.18      val T = Type (t, map TFree args);
    1.19      val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
    1.20