diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_dt_data.ML
--- a/Nominal/nominal_dt_data.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_data.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -25,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      : Datatype.spec list,
+    {dts      : Old_Datatype.spec list,
      cn_names : string list,
      cn_tys   : (string * string) list,
      bn_funs  : (binding * typ * mixfix) list,
@@ -34,7 +34,7 @@
 
   datatype raw_dt_info = RawDtInfo of
     {raw_dt_names         : string list,
-     raw_dts              : Datatype.spec list,
+     raw_dts              : Old_Datatype.spec list,
      raw_tys              : typ list,
      raw_ty_args          : (string * sort) list,
      raw_cns_info         : cns_info list,
@@ -111,7 +111,7 @@
 
 
 datatype user_data = UserData of
-  {dts      : Datatype.spec list,
+  {dts      : Old_Datatype.spec list,
    cn_names : string list,
    cn_tys   : (string * string) list,
    bn_funs  : (binding * typ * mixfix) list,
@@ -120,7 +120,7 @@
 
 datatype raw_dt_info = RawDtInfo of
   {raw_dt_names         : string list,
-   raw_dts              : Datatype.spec list,
+   raw_dts              : Old_Datatype.spec list,
    raw_tys              : typ list,
    raw_ty_args          : (string * sort) list,
    raw_cns_info         : cns_info list,