src/HOL/Tools/datatype_aux.ML
changeset 8404 4b39358f9810
parent 8324 df7dccddc3de
child 8435 51a040fd2200
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Mar 09 22:58:23 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Mar 10 01:13:37 2000 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4        DtTFree of string
     1.5      | DtType of string * (dtyp list)
     1.6      | DtRec of int;
     1.7 -
     1.8 +  type descr
     1.9    type datatype_info
    1.10  
    1.11    exception Datatype
    1.12 @@ -152,9 +152,11 @@
    1.13  
    1.14  (* information about datatypes *)
    1.15  
    1.16 +type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
    1.17 +
    1.18  type datatype_info =
    1.19    {index : int,
    1.20 -   descr : (int * (string * dtyp list * (string * dtyp list) list)) list,
    1.21 +   descr : descr,
    1.22     rec_names : string list,
    1.23     rec_rewrites : thm list,
    1.24     case_name : string,