--- a/Nominal/nominal_dt_data.ML	Mon Jul 11 12:23:24 2011 +0100
+++ b/Nominal/nominal_dt_data.ML	Mon Jul 11 12:23:44 2011 +0100
@@ -5,11 +5,21 @@
 
 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
+
+  (* binding modes and binding clauses *)
+  datatype bmode = Lst | Res | Set
+  datatype bclause = BC of bmode * (term option * int) list * int list
+
   type info =
-   {inject : thm list,
-    distinct : thm list,
-    strong_inducts : thm list,
-    strong_exhaust : thm list}
+    {inject : thm list,
+     distinct : thm list,
+     strong_inducts : thm list,
+     strong_exhaust : thm list}
 
   val get_all_info: Proof.context -> (string * info) list
   val get_info: Proof.context -> string -> info option
@@ -17,6 +27,29 @@
   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,
+     raw_tys              : typ list,
+     raw_ty_args          : (string * sort) list,
+     raw_cns_info         : cns_info list,
+     raw_all_cns          : term list list,
+     raw_inject_thms      : thm list,
+     raw_distinct_thms    : thm list,
+     raw_induct_thm       : thm,
+     raw_induct_thms      : thm list,
+     raw_exhaust_thms     : thm list,
+     raw_size_trms        : term list,
+     raw_size_thms        : thm list}
+
   datatype alpha_result = AlphaResult of
     {alpha_names      : string list,
      alpha_trms       : term list,
@@ -33,6 +66,24 @@
 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
+   int * term option - is number of the corresponding argument with possibly
+                       recursive call with bn-function term 
+*)  
+type bn_info = term * int * (int * term option) list list
+
+datatype bmode = Lst | Res | Set
+datatype bclause = BC of bmode * (term option * int) list * int list
+
 
 (* information generated by nominal_datatype *)
 type info =
@@ -68,6 +119,30 @@
   map aux ty_names
 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,
+   raw_tys              : typ list,
+   raw_ty_args          : (string * sort) list,
+   raw_cns_info         : cns_info list,
+   raw_all_cns          : term list list,
+   raw_inject_thms      : thm list,
+   raw_distinct_thms    : thm list,
+   raw_induct_thm       : thm,
+   raw_induct_thms      : thm list,
+   raw_exhaust_thms     : thm list,
+   raw_size_trms        : term list,
+   raw_size_thms        : thm list}
+
 datatype alpha_result = AlphaResult of
   {alpha_names      : string list,
    alpha_trms       : term list,
@@ -79,5 +154,4 @@
    alpha_cases      : thm list,
    alpha_raw_induct : thm}
 
-
 end
\ No newline at end of file