diff -r 37c0d7953cba -r 116f9ba4f59f Nominal/nominal_dt_data.ML
--- a/Nominal/nominal_dt_data.ML	Wed Jun 29 19:21:26 2011 +0100
+++ b/Nominal/nominal_dt_data.ML	Wed Jun 29 23:08:44 2011 +0100
@@ -16,11 +16,24 @@
   val the_info: Proof.context -> string -> info 
   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 alpha_result = AlphaResult of
+    {alpha_names      : string list,
+     alpha_trms       : term list,
+     alpha_tys        : typ list,
+     alpha_bn_names   : string list,
+     alpha_bn_trms    : term list,
+     alpha_bn_tys     : typ list,
+     alpha_intros     : thm list,
+     alpha_cases      : thm list,
+     alpha_raw_induct : thm}
+   
 end
 
 structure Nominal_Dt_Data: NOMINAL_DT_DATA =
 struct
 
+
 (* information generated by nominal_datatype *)
 type info =
    {inject : thm list,
@@ -55,5 +68,16 @@
   map aux ty_names
 end
 
+datatype alpha_result = AlphaResult of
+  {alpha_names      : string list,
+   alpha_trms       : term list,
+   alpha_tys        : typ list,
+   alpha_bn_names   : string list,
+   alpha_bn_trms    : term list,
+   alpha_bn_tys     : typ list,
+   alpha_intros     : thm list,
+   alpha_cases      : thm list,
+   alpha_raw_induct : thm}
+
 
 end
\ No newline at end of file