# HG changeset patch
# User haftmann
# Date 1245763954 -7200
# Node ID cfbe9609ceb1863a34ce460dff203e3cdd4f0994
# Parent  2b041d16cc13c5f3ca8ff01c61f2fb137b31812b
add_datatypes does not yield particular rules any longer

diff -r 2b041d16cc13 -r cfbe9609ceb1 src/HOL/Nominal/nominal.ML
--- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 14:51:21 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 15:32:34 2009 +0200
@@ -241,13 +241,12 @@
         map replace_types cargs, NoSyn)) constrs)) dts';
 
     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
-    val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
 
-    val ((dt_names, {induction, ...}),thy1) =
+    val (full_new_type_names',thy1) =
       Datatype.add_datatype config new_type_names' dts'' thy;
 
-    val SOME {descr, ...} = Symtab.lookup
-      (Datatype.get_datatypes thy1) (hd full_new_type_names');
+    val {descr, induction, ...} =
+      Datatype.the_datatype thy1 (hd full_new_type_names');
     fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
     val big_name = space_implode "_" new_type_names;
diff -r 2b041d16cc13 -r cfbe9609ceb1 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 14:51:21 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 15:32:34 2009 +0200
@@ -101,9 +101,10 @@
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
           let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
-              val ((dt_names, {inject,case_thms,...}),thy1) = Datatype.add_datatype
-                Datatype.default_config [ak] [dt] thy
-              val inject_flat = flat inject
+              val (dt_names, thy1) = Datatype.add_datatype
+                Datatype.default_config [ak] [dt] thy;
+            
+              val injects = maps (#inject o Datatype.the_datatype thy1) dt_names;
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
               
@@ -115,7 +116,7 @@
                   (Const (@{const_name "inj_on"},inj_on_type) $ 
                          Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat})
 
-              val simp1 = @{thm inj_on_def}::inject_flat
+              val simp1 = @{thm inj_on_def} :: injects;
               
               val proof1 = fn _ => EVERY [simp_tac (HOL_basic_ss addsimps simp1) 1,
                                           rtac @{thm ballI} 1,
diff -r 2b041d16cc13 -r cfbe9609ceb1 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 14:51:21 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 15:32:34 2009 +0200
@@ -8,11 +8,7 @@
 sig
   include DATATYPE_COMMON
   val add_datatype : config -> string list -> (string list * binding * mixfix *
-    (binding * typ list * mixfix) list) list -> theory ->
-     (string list * {inject : thm list list,
-      rec_thms : thm list,
-      case_thms : thm list list,
-      induction : thm}) * theory
+    (binding * typ list * mixfix) list) list -> theory -> string list * theory
   val datatype_cmd : string list -> (string list * binding * mixfix *
     (binding * string list * mixfix) list) list -> theory -> theory
   val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
@@ -381,12 +377,7 @@
       |> Sign.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
       |> DatatypeInterpretation.data (config, map fst dt_infos);
-  in
-    ((dt_names, {inject = inject,
-      rec_thms = rec_thms,
-      case_thms = case_thms,
-      induction = induct}), thy12)
-  end;
+  in (dt_names, thy12) end;
 
 
 (*********************** declare existing type as datatype *********************)
diff -r 2b041d16cc13 -r cfbe9609ceb1 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 14:51:21 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 15:32:34 2009 +0200
@@ -305,15 +305,17 @@
 
     (** datatype representing computational content of inductive set **)
 
-    val ((dummies, (dt_names_rules)), thy2) =
+    val ((dummies, some_dt_names), thy2) =
       thy1
       |> add_dummies (Datatype.add_datatype
            { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
            (map (pair false) dts) []
       ||> Extraction.add_typeof_eqns_i ty_eqs
       ||> Extraction.add_realizes_eqns_i rlz_eqs;
-    val rec_thms = these (Option.map (#rec_thms o snd) dt_names_rules);
-    val case_thms = these (Option.map (#case_thms o snd) dt_names_rules);
+    val dt_names = these some_dt_names;
+    val case_thms = map (#case_rewrites o Datatype.the_datatype thy2) dt_names;
+    val rec_thms = if null dt_names then []
+      else (#rec_rewrites o Datatype.the_datatype thy2) (hd dt_names);
     val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
       HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
     val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>