author | wenzelm |
Fri, 14 Dec 2001 11:50:19 +0100 | |
changeset 12493 | de2575b6cd38 |
parent 12492 | a4dd02e744e0 |
child 12494 | 58848edad3c4 |
--- 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 =