src/Pure/type_infer.ML

     fun elim (r as ref (Param S), x) = r := mk_var (x, S)
       | elim _ = ();
 
     val used' = fold add_names ts (fold add_namesT Ts used);
     val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
-    val names = Term.invent_names used' (prfx ^ "'a") (length parms);
+    val names = Name.invent_list used' (prfx ^ "'a") (length parms);
   in
     ListPair.app elim (parms, names);
     (map simple_typ_of Ts, map simple_term_of ts)
   end;