changeset 12493 | de2575b6cd38 |
parent 12371 | 80ca9058db95 |
child 12694 | 9950c1ce9d24 |
--- a/src/Pure/axclass.ML Thu Dec 13 19:05:10 2001 +0100 +++ b/src/Pure/axclass.ML Fri Dec 14 11:50:19 2001 +0100 @@ -98,7 +98,7 @@ fun mk_arity (t, ss, c) = let - val tfrees = ListPair.map TFree (Term.invent_names (length ss) "'", ss); + val tfrees = ListPair.map TFree (Term.invent_type_names [] (length ss), ss); in Logic.mk_inclass (Type (t, tfrees), c) end; fun dest_arity tm =