--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_dt_data.ML	Thu Jun 23 13:09:17 2011 +0100
@@ -0,0 +1,59 @@
+(* Author: Christian Urban
+
+   data about nominal datatypes 
+*)
+
+signature NOMINAL_DT_DATA =
+sig
+  type info =
+   {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
+  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
+end
+
+structure Nominal_Dt_Data: NOMINAL_DT_DATA =
+struct
+
+(* information generated by nominal_datatype *)
+type info =
+   {inject : thm list,
+    distinct : thm list,
+    strong_inducts : thm list,
+    strong_exhaust : thm list}
+
+structure NominalData = Generic_Data
+ (type T = info Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+  val merge = Symtab.merge (K true))
+
+val get_all_info = Symtab.dest o NominalData.get o Context.Proof
+val get_info = Symtab.lookup o NominalData.get o Context.Proof
+val register_info = NominalData.map o Symtab.update
+
+fun the_info thy name =
+  (case get_info thy name of
+    SOME info => info
+  | NONE => error ("Unknown nominal datatype " ^ quote name))
+
+fun mk_infos ty_names inject distinct strong_inducts strong_exhaust =
+let
+  fun aux ty_name =
+    (ty_name, {inject = inject,
+               distinct = distinct,
+               strong_inducts = strong_inducts,
+               strong_exhaust = strong_exhaust 
+              })
+in
+  map aux ty_names
+end
+
+
+end
\ No newline at end of file