add_datatype interface yields type names and less rules

--- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 12:09:30 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 14:50:34 2009 +0200
@@ -243,7 +243,7 @@
     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 ({induction, ...},thy1) =
+    val ((dt_names, {induction, ...}),thy1) =
       Datatype.add_datatype config new_type_names' dts'' thy;
 
     val SOME {descr, ...} = Symtab.lookup

--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 12:09:30 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 14:50:34 2009 +0200
@@ -101,7 +101,7 @@
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
           let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
-              val ({inject,case_thms,...},thy1) = Datatype.add_datatype
+              val ((dt_names, {inject,case_thms,...}),thy1) = Datatype.add_datatype
                 Datatype.default_config [ak] [dt] thy
               val inject_flat = flat inject
               val ak_type = Type (Sign.intern_type thy1 ak,[])

--- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 12:09:30 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 14:50:34 2009 +0200
@@ -7,19 +7,15 @@
 signature DATATYPE =
 sig
   include DATATYPE_COMMON
-  type rules = {distinct : thm list list,
-    inject : thm list list,
-    exhaustion : thm list,
-    rec_thms : thm list,
-    case_thms : thm list list,
-    split_thms : (thm * thm) list,
-    induction : thm,
-    simps : thm list}
   val add_datatype : config -> string list -> (string list * binding * mixfix *
-    (binding * typ list * mixfix) list) list -> theory -> rules * theory
+    (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
   val datatype_cmd : string list -> (string list * binding * mixfix *
     (binding * string list * mixfix) list) list -> theory -> theory
-  val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
+  val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
     -> string list option -> term list -> theory -> Proof.state
   val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
   val get_datatypes : theory -> info Symtab.table
@@ -334,15 +330,6 @@
     case_cong = case_cong,
     weak_case_cong = weak_case_cong});
 
-type rules = {distinct : thm list list,
-  inject : thm list list,
-  exhaustion : thm list,
-  rec_thms : thm list,
-  case_thms : thm list list,
-  split_thms : (thm * thm) list,
-  induction : thm,
-  simps : thm list}
-
 structure DatatypeInterpretation = InterpretationFun
   (type T = config * string list val eq: T * T -> bool = eq_snd op =);
 fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
@@ -377,10 +364,11 @@
 
     val dt_infos = map
       (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
-      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
+      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
         casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
+    val dt_names = map fst dt_infos;
 
     val thy12 =
       thy10
@@ -394,14 +382,10 @@
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
       |> DatatypeInterpretation.data (config, map fst dt_infos);
   in
-    ({distinct = distinct,
-      inject = inject,
-      exhaustion = casedist_thms,
+    ((dt_names, {inject = inject,
       rec_thms = rec_thms,
       case_thms = case_thms,
-      split_thms = split_thms,
-      induction = induct,
-      simps = simps}, thy12)
+      induction = induct}), thy12)
   end;
 
 
@@ -457,6 +441,7 @@
         map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
+    val dt_names = map fst dt_infos;
 
     val thy11 =
       thy10
@@ -468,17 +453,8 @@
       |> 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
-    ({distinct = distinct,
-      inject = inject,
-      exhaustion = casedist_thms,
-      rec_thms = rec_thms,
-      case_thms = case_thms,
-      split_thms = split_thms,
-      induction = induct',
-      simps = simps}, thy11)
-  end;
+      |> DatatypeInterpretation.data (config, dt_names);
+  in (dt_names, thy11) end;
 
 fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
   let

--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 12:09:30 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 14:50:34 2009 +0200
@@ -305,16 +305,17 @@
 
     (** datatype representing computational content of inductive set **)
 
-    val ((dummies, dt_info), thy2) =
+    val ((dummies, (dt_names_rules)), 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;
-    fun get f = (these oo Option.map) f;
+    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 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) (get #rec_thms dt_info));
+      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
     val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
       if member (op =) rsets s then
         let
@@ -324,7 +325,7 @@
           HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
         end
       else (replicate (length rs) Extraction.nullt, (recs, dummies)))
-        rss (get #rec_thms dt_info, dummies);
+        rss (rec_thms, dummies);
     val rintrs = map (fn (intr, c) => Envir.eta_contract
       (Extraction.realizes_of thy2 vs
         (if c = Extraction.nullt then c else list_comb (c, map Var (rev
@@ -386,8 +387,7 @@
           end) (rlzs ~~ rnames);
         val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
           (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
-        val rews = map mk_meta_eq
-          (fst_conv :: snd_conv :: get #rec_thms dt_info);
+        val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
         val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
           [rtac (#raw_induct ind_info) 1,
            rewrite_goals_tac rews,
@@ -417,7 +417,7 @@
     (** realizer for elimination rules **)
 
     val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
-      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
+      HOLogic.dest_Trueprop o prop_of o hd) case_thms;
 
     fun add_elim_realizer Ps
       (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
@@ -476,7 +476,7 @@
     val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
       add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
         (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
-           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
+           elimps ~~ case_thms ~~ case_names ~~ dummies)
 
   in Sign.restore_naming thy thy6 end;