src/Pure/type_infer.ML
changeset 20076 def4ad161528
parent 19577 fdb3642feb49
child 20161 b8b1d4a380aa
     1.1 --- a/src/Pure/type_infer.ML	Tue Jul 11 12:17:00 2006 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Jul 11 12:17:01 2006 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4  
     1.5      val used' = fold add_names ts (fold add_namesT Ts used);
     1.6      val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
     1.7 -    val names = Term.invent_names used' (prfx ^ "'a") (length parms);
     1.8 +    val names = Name.invent_list used' (prfx ^ "'a") (length parms);
     1.9    in
    1.10      ListPair.app elim (parms, names);
    1.11      (map simple_typ_of Ts, map simple_term_of ts)