src/Pure/logic.ML
changeset 24848 5dbbd33c3236
parent 24258 2f399483535a
child 25939 ddea202704b4
     1.1 --- a/src/Pure/logic.ML	Thu Oct 04 20:29:13 2007 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Oct 04 20:29:24 2007 +0200
     1.3 @@ -238,7 +238,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.invent_list [] "'a" (length Ss), Ss))
     1.8 +  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
     1.9    in map (fn c => mk_inclass (T, c)) S end;
    1.10  
    1.11  fun dest_arity tm =