Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_dt_data.ML
changeset 3239 67370521c09c
parent 3065 51ef8a3cb6ef
child 3245 017e33849f4d 
--- 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,
nominal2