--- a/Nominal/Nominal2.thy	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/Nominal2.thy	Wed Jun 22 12:18:22 2011 +0100
@@ -10,8 +10,12 @@
      ("nominal_function_core.ML")
      ("nominal_mutual.ML")
      ("nominal_function.ML")
+     ("nominal_dt_data.ML")
 begin
 
+use "nominal_dt_data.ML"
+ML {* open Nominal_Dt_Data *}
+
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
 
@@ -139,6 +143,8 @@
 
 
 ML {*
+(* definition of the raw datatype *)
+
 fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
 let
   val thy = Local_Theory.exit_global lthy
@@ -459,7 +465,10 @@
   fun thms_suffix s = Binding.qualified true s thms_name 
   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
+  val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms
+
   val (_, lthy9') = lthyC
+     |> Local_Theory.declaration false (K (fold register_info infos))
      |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) 
      ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs)