1.1 --- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 12:09:30 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 14:50:34 2009 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     1.5      val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
     1.6  
     1.7 -    val ({induction, ...},thy1) =
     1.8 +    val ((dt_names, {induction, ...}),thy1) =
     1.9        Datatype.add_datatype config new_type_names' dts'' thy;
    1.10  
    1.11      val SOME {descr, ...} = Symtab.lookup

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

     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 12:09:30 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 14:50:34 2009 +0200
     3.3 @@ -7,19 +7,15 @@
     3.4  signature DATATYPE =
     3.5  sig
     3.6    include DATATYPE_COMMON
     3.7 -  type rules = {distinct : thm list list,
     3.8 -    inject : thm list list,
     3.9 -    exhaustion : thm list,
    3.10 -    rec_thms : thm list,
    3.11 -    case_thms : thm list list,
    3.12 -    split_thms : (thm * thm) list,
    3.13 -    induction : thm,
    3.14 -    simps : thm list}
    3.15    val add_datatype : config -> string list -> (string list * binding * mixfix *
    3.16 -    (binding * typ list * mixfix) list) list -> theory -> rules * theory
    3.17 +    (binding * typ list * mixfix) list) list -> theory ->
    3.18 +     (string list * {inject : thm list list,
    3.19 +      rec_thms : thm list,
    3.20 +      case_thms : thm list list,
    3.21 +      induction : thm}) * theory
    3.22    val datatype_cmd : string list -> (string list * binding * mixfix *
    3.23      (binding * string list * mixfix) list) list -> theory -> theory
    3.24 -  val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
    3.25 +  val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    3.26      -> string list option -> term list -> theory -> Proof.state
    3.27    val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
    3.28    val get_datatypes : theory -> info Symtab.table
    3.29 @@ -334,15 +330,6 @@
    3.30      case_cong = case_cong,
    3.31      weak_case_cong = weak_case_cong});
    3.32  
    3.33 -type rules = {distinct : thm list list,
    3.34 -  inject : thm list list,
    3.35 -  exhaustion : thm list,
    3.36 -  rec_thms : thm list,
    3.37 -  case_thms : thm list list,
    3.38 -  split_thms : (thm * thm) list,
    3.39 -  induction : thm,
    3.40 -  simps : thm list}
    3.41 -
    3.42  structure DatatypeInterpretation = InterpretationFun
    3.43    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    3.44  fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    3.45 @@ -377,10 +364,11 @@
    3.46  
    3.47      val dt_infos = map
    3.48        (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
    3.49 -      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
    3.50 +      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
    3.51          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    3.52  
    3.53      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    3.54 +    val dt_names = map fst dt_infos;
    3.55  
    3.56      val thy12 =
    3.57        thy10
    3.58 @@ -394,14 +382,10 @@
    3.59        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    3.60        |> DatatypeInterpretation.data (config, map fst dt_infos);
    3.61    in
    3.62 -    ({distinct = distinct,
    3.63 -      inject = inject,
    3.64 -      exhaustion = casedist_thms,
    3.65 +    ((dt_names, {inject = inject,
    3.66        rec_thms = rec_thms,
    3.67        case_thms = case_thms,
    3.68 -      split_thms = split_thms,
    3.69 -      induction = induct,
    3.70 -      simps = simps}, thy12)
    3.71 +      induction = induct}), thy12)
    3.72    end;
    3.73  
    3.74  
    3.75 @@ -457,6 +441,7 @@
    3.76          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    3.77  
    3.78      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    3.79 +    val dt_names = map fst dt_infos;
    3.80  
    3.81      val thy11 =
    3.82        thy10
    3.83 @@ -468,17 +453,8 @@
    3.84        |> Sign.parent_path
    3.85        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    3.86        |> snd
    3.87 -      |> DatatypeInterpretation.data (config, map fst dt_infos);
    3.88 -  in
    3.89 -    ({distinct = distinct,
    3.90 -      inject = inject,
    3.91 -      exhaustion = casedist_thms,
    3.92 -      rec_thms = rec_thms,
    3.93 -      case_thms = case_thms,
    3.94 -      split_thms = split_thms,
    3.95 -      induction = induct',
    3.96 -      simps = simps}, thy11)
    3.97 -  end;
    3.98 +      |> DatatypeInterpretation.data (config, dt_names);
    3.99 +  in (dt_names, thy11) end;
   3.100  
   3.101  fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
   3.102    let

     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 12:09:30 2009 +0200
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 14:50:34 2009 +0200
     4.3 @@ -305,16 +305,17 @@
     4.4  
     4.5      (** datatype representing computational content of inductive set **)
     4.6  
     4.7 -    val ((dummies, dt_info), thy2) =
     4.8 +    val ((dummies, (dt_names_rules)), thy2) =
     4.9        thy1
    4.10        |> add_dummies (Datatype.add_datatype
    4.11             { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
    4.12             (map (pair false) dts) []
    4.13        ||> Extraction.add_typeof_eqns_i ty_eqs
    4.14        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    4.15 -    fun get f = (these oo Option.map) f;
    4.16 +    val rec_thms = these (Option.map (#rec_thms o snd) dt_names_rules);
    4.17 +    val case_thms = these (Option.map (#case_thms o snd) dt_names_rules);
    4.18      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
    4.19 -      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
    4.20 +      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
    4.21      val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
    4.22        if member (op =) rsets s then
    4.23          let
    4.24 @@ -324,7 +325,7 @@
    4.25            HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
    4.26          end
    4.27        else (replicate (length rs) Extraction.nullt, (recs, dummies)))
    4.28 -        rss (get #rec_thms dt_info, dummies);
    4.29 +        rss (rec_thms, dummies);
    4.30      val rintrs = map (fn (intr, c) => Envir.eta_contract
    4.31        (Extraction.realizes_of thy2 vs
    4.32          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    4.33 @@ -386,8 +387,7 @@
    4.34            end) (rlzs ~~ rnames);
    4.35          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
    4.36            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
    4.37 -        val rews = map mk_meta_eq
    4.38 -          (fst_conv :: snd_conv :: get #rec_thms dt_info);
    4.39 +        val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
    4.40          val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
    4.41            [rtac (#raw_induct ind_info) 1,
    4.42             rewrite_goals_tac rews,
    4.43 @@ -417,7 +417,7 @@
    4.44      (** realizer for elimination rules **)
    4.45  
    4.46      val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
    4.47 -      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
    4.48 +      HOLogic.dest_Trueprop o prop_of o hd) case_thms;
    4.49  
    4.50      fun add_elim_realizer Ps
    4.51        (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
    4.52 @@ -476,7 +476,7 @@
    4.53      val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
    4.54        add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
    4.55          (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
    4.56 -           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
    4.57 +           elimps ~~ case_thms ~~ case_names ~~ dummies)
    4.58  
    4.59    in Sign.restore_naming thy thy6 end;
    4.60