src/Pure/type_infer.ML
changeset 24848 5dbbd33c3236
parent 24764 4c2b872f8cf6
child 27263 a6b7f934fbc4
     1.1 --- a/src/Pure/type_infer.ML	Thu Oct 04 20:29:13 2007 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Oct 04 20:29:24 2007 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4      fun subst_param (xi, S) (inst, used) =
     1.5        if is_param xi then
     1.6          let
     1.7 -          val [a] = Name.invents used "'a" 1;
     1.8 +          val [a] = Name.invents used Name.aT 1;
     1.9            val used' = Name.declare a used;
    1.10          in (((xi, S), TFree (a, S)) :: inst, used') end
    1.11        else (inst, used);
    1.12 @@ -237,7 +237,7 @@
    1.13  
    1.14      val used' = fold add_names ts (fold add_namesT Ts used);
    1.15      val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
    1.16 -    val names = Name.invents used' (prfx ^ "'a") (length parms);
    1.17 +    val names = Name.invents used' (prfx ^ Name.aT) (length parms);
    1.18    in
    1.19      ListPair.app elim (parms, names);
    1.20      (map simple_typ_of Ts, map simple_term_of ts)