src/Pure/logic.ML
changeset 43329 84472e198515
parent 37230 7b548f137276
child 45328 e5b33eecbf6e
     1.1 --- a/src/Pure/logic.ML	Wed Jun 08 22:16:21 2011 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jun 09 20:22:22 2011 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4  fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
     1.5  
     1.6  fun mk_arities (t, Ss, S) =
     1.7 -  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
     1.8 +  let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
     1.9    in map (fn c => mk_of_class (T, c)) S end;
    1.10  
    1.11  fun dest_arity tm =
    1.12 @@ -279,7 +279,7 @@
    1.13      val extra = fold (Sorts.remove_sort o #2) present shyps;
    1.14  
    1.15      val n = length present;
    1.16 -    val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n;
    1.17 +    val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
    1.18  
    1.19      val present_map =
    1.20        map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;