src/Pure/type_infer.ML
changeset 43329 84472e198515
parent 42405 13ecdb3057d8
child 53672 df8068269e90
     1.1 --- a/src/Pure/type_infer.ML	Wed Jun 08 22:16:21 2011 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Jun 09 20:22:22 2011 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4      val used =
     1.5        (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
     1.6      val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
     1.7 -    val names = Name.invents used ("?" ^ Name.aT) (length parms);
     1.8 +    val names = Name.invent used ("?" ^ Name.aT) (length parms);
     1.9      val tab = Vartab.make (parms ~~ names);
    1.10  
    1.11      fun finish_typ T =
    1.12 @@ -117,7 +117,7 @@
    1.13      fun subst_param (xi, S) (inst, used) =
    1.14        if is_param xi then
    1.15          let
    1.16 -          val [a] = Name.invents used Name.aT 1;
    1.17 +          val [a] = Name.invent used Name.aT 1;
    1.18            val used' = Name.declare a used;
    1.19          in (((xi, S), TFree (a, S)) :: inst, used') end
    1.20        else (inst, used);