author | webertj |
Tue, 07 Dec 2004 14:42:08 +0100 | |
changeset 15379 | 830239e6eb73 |
parent 15378 | b1c5add0a65e |
child 15380 | 455cfa766dad |
--- a/src/HOL/Tools/datatype_aux.ML Tue Dec 07 12:13:17 2004 +0100 +++ b/src/HOL/Tools/datatype_aux.ML Tue Dec 07 14:42:08 2004 +0100 @@ -175,6 +175,7 @@ (* information about datatypes *) +(* index, datatype name, type arguments (DtTFree's), constructor name, types of constructor's arguments *) type descr = (int * (string * dtyp list * (string * dtyp list) list)) list; type datatype_info =