diff -r d0f83a35950e -r 9bd97ed202f7 Nominal/nominal_dt_data.ML
--- a/Nominal/nominal_dt_data.ML	Thu Jul 07 16:17:03 2011 +0200
+++ b/Nominal/nominal_dt_data.ML	Fri Jul 08 05:04:23 2011 +0200
@@ -27,6 +27,14 @@
   val register_info: (string * info) -> Context.generic -> Context.generic
   val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
 
+  datatype user_data = UserData of
+    {dts      : dt_info,
+     cn_names : string list,
+     cn_tys   : (string * string) list,
+     bn_funs  : (binding * typ * mixfix) list,
+     bn_eqs   : (Attrib.binding * term) list,
+     bclauses : bclause list list list}
+
   datatype raw_dt_info = RawDtInfo of
     {raw_dt_names         : string list,
      raw_dts              : dt_info,
@@ -112,6 +120,14 @@
 end
 
 
+datatype user_data = UserData of
+  {dts      : dt_info,
+   cn_names : string list,
+   cn_tys   : (string * string) list,
+   bn_funs  : (binding * typ * mixfix) list,
+   bn_eqs   : (Attrib.binding * term) list,
+   bclauses : bclause list list list}
+
 datatype raw_dt_info = RawDtInfo of
   {raw_dt_names         : string list,
    raw_dts              : dt_info,