src/Pure/logic.ML

--- a/src/Pure/logic.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/logic.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -238,7 +238,7 @@
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
+  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
   in map (fn c => mk_inclass (T, c)) S end;
 
 fun dest_arity tm =