diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/nominal_dt_data.ML
--- a/Nominal/nominal_dt_data.ML	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/nominal_dt_data.ML	Thu Dec 15 16:20:42 2011 +0000
@@ -5,9 +5,6 @@
 
 signature NOMINAL_DT_DATA =
 sig
-  (* info of raw datatypes *)
-  type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
-
   (* info of raw binding functions *)
   type bn_info = term * int * (int * term option) list list
 
@@ -28,7 +25,7 @@
   val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
 
   datatype user_data = UserData of
-    {dts      : dt_info,
+    {dts      : Datatype.spec list,
      cn_names : string list,
      cn_tys   : (string * string) list,
      bn_funs  : (binding * typ * mixfix) list,
@@ -37,7 +34,7 @@
 
   datatype raw_dt_info = RawDtInfo of
     {raw_dt_names         : string list,
-     raw_dts              : dt_info,
+     raw_dts              : Datatype.spec list,
      raw_tys              : typ list,
      raw_ty_args          : (string * sort) list,
      raw_cns_info         : cns_info list,
@@ -66,13 +63,6 @@
 structure Nominal_Dt_Data: NOMINAL_DT_DATA =
 struct
 
-(* string list      - type variables of a datatype
-   binding          - name of the datatype
-   mixfix           - its mixfix
-   (binding * typ list * mixfix) list  - datatype constructors of the type
-*)  
-type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
-
 
 (* term              - is constant of the bn-function 
    int               - is datatype number over which the bn-function is defined
@@ -121,7 +111,7 @@
 
 
 datatype user_data = UserData of
-  {dts      : dt_info,
+  {dts      : Datatype.spec list,
    cn_names : string list,
    cn_tys   : (string * string) list,
    bn_funs  : (binding * typ * mixfix) list,
@@ -130,7 +120,7 @@
 
 datatype raw_dt_info = RawDtInfo of
   {raw_dt_names         : string list,
-   raw_dts              : dt_info,
+   raw_dts              : Datatype.spec list,
    raw_tys              : typ list,
    raw_ty_args          : (string * sort) list,
    raw_cns_info         : cns_info list,