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 =