src/Pure/axclass.ML
changeset 11353 7f6eff7bc97a
parent 11101 014e7b5c77ba
child 11539 0f17da240450
--- a/src/Pure/axclass.ML	Thu May 31 17:24:56 2001 +0200
+++ b/src/Pure/axclass.ML	Thu May 31 17:57:02 2001 +0200
@@ -103,8 +103,7 @@
 
 fun mk_arity (t, ss, c) =
   let
-    val names = tl (variantlist (replicate (length ss + 1) "'", []));
-    val tfrees = ListPair.map TFree (names, ss);
+    val tfrees = ListPair.map TFree (Term.invent_names (length ss + 1) "'", ss);
   in Logic.mk_inclass (Type (t, tfrees), c) end;
 
 fun dest_arity tm =