# HG changeset patch
# User haftmann
# Date 1245784059 -7200
# Node ID c8a590599cb595a185216569832da12a49472789
# Parent  d78e5cff9a9ff585dd08f9364ca513a265a9a1a3# Parent  496c86f5f9e93870af61d284fe90b9897585cf69
merged

diff -r d78e5cff9a9f -r c8a590599cb5 NEWS
--- a/NEWS	Tue Jun 23 21:05:51 2009 +0200
+++ b/NEWS	Tue Jun 23 21:07:39 2009 +0200
@@ -52,10 +52,12 @@
 
 INCOMPATIBILITY.
 
-
 * NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
 If possible, use NewNumberTheory, not NumberTheory.
 
+* Simplified interfaces of datatype module.  INCOMPATIBILITY.
+
+
 *** ML ***
 
 * Eliminated old Attrib.add_attributes, Method.add_methods and related
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Inductive.thy	Tue Jun 23 21:07:39 2009 +0200
@@ -364,7 +364,7 @@
   fun fun_tr ctxt [cs] =
     let
       val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
-      val ft = DatatypeCase.case_tr true Datatype.datatype_of_constr
+      val ft = DatatypeCase.case_tr true Datatype.info_of_constr
                  ctxt [x, cs]
     in lambda x ft end
 in [("_lam_pats_syntax", fun_tr)] end
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/List.thy	Tue Jun 23 21:07:39 2009 +0200
@@ -363,7 +363,7 @@
       val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
                                         $ NilC;
       val cs = Syntax.const "_case2" $ case1 $ case2
-      val ft = DatatypeCase.case_tr false Datatype.datatype_of_constr
+      val ft = DatatypeCase.case_tr false Datatype.info_of_constr
                  ctxt [x, cs]
     in lambda x ft end;
 
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Nominal/nominal.ML
--- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 21:07:39 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 ({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_info 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 d78e5cff9a9f -r c8a590599cb5 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 21:07:39 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 ({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_info 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 d78e5cff9a9f -r c8a590599cb5 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -340,7 +340,7 @@
   | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
   | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
 
-fun is_datatype thy n = is_some (Symtab.lookup (Datatype.get_datatypes thy) n);
+fun is_datatype thy = is_some o Datatype.get_info thy;
 
 fun mk_map "List.list" = Syntax.const "List.map"
   | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -7,31 +7,23 @@
 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 * 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
-  val get_datatype : theory -> string -> info option
-  val the_datatype : theory -> string -> info
-  val datatype_of_constr : theory -> string -> info option
-  val datatype_of_case : theory -> string -> info option
-  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
-  val the_datatype_descr : theory -> string list
+  val get_info : theory -> string -> info option
+  val the_info : theory -> string -> info
+  val the_descr : theory -> string list
     -> descr * (string * sort) list * string list
       * (string list * string list) * (typ list * typ list)
-  val get_datatype_constrs : theory -> string -> (string * typ) list option
+  val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
+  val get_constrs : theory -> string -> (string * typ) list option
+  val get_all : theory -> info Symtab.table
+  val info_of_constr : theory -> string -> info option
+  val info_of_case : theory -> string -> info option
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
   val distinct_simproc : simproc
   val make_case :  Proof.context -> bool -> string list -> term ->
@@ -69,7 +61,7 @@
      cases = Symtab.merge (K true) (cases1, cases2)};
 );
 
-val get_datatypes = #types o DatatypesData.get;
+val get_all = #types o DatatypesData.get;
 val map_datatypes = DatatypesData.map;
 
 
@@ -85,23 +77,23 @@
        (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
        cases});
 
-val get_datatype = Symtab.lookup o get_datatypes;
+val get_info = Symtab.lookup o get_all;
 
-fun the_datatype thy name = (case get_datatype thy name of
+fun the_info thy name = (case get_info thy name of
       SOME info => info
     | NONE => error ("Unknown datatype " ^ quote name));
 
-val datatype_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
-val datatype_of_case = Symtab.lookup o #cases o DatatypesData.get;
+val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
+val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
 
-fun get_datatype_descr thy dtco =
-  get_datatype thy dtco
+fun get_info_descr thy dtco =
+  get_info thy dtco
   |> Option.map (fn info as { descr, index, ... } =>
        (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
 
-fun the_datatype_spec thy dtco =
+fun the_spec thy dtco =
   let
-    val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
+    val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
     val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
     val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
       o DatatypeAux.dest_DtTFree) dtys;
@@ -109,9 +101,9 @@
       (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
   in (sorts, cos) end;
 
-fun the_datatype_descr thy (raw_tycos as raw_tyco :: _) =
+fun the_descr thy (raw_tycos as raw_tyco :: _) =
   let
-    val info = the_datatype thy raw_tyco;
+    val info = the_info thy raw_tyco;
     val descr = #descr info;
 
     val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
@@ -137,8 +129,8 @@
 
   in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
 
-fun get_datatype_constrs thy dtco =
-  case try (the_datatype_spec thy) dtco
+fun get_constrs thy dtco =
+  case try (the_spec thy) dtco
    of SOME (sorts, cos) =>
         let
           fun subst (v, sort) = TVar ((v, 0), sort);
@@ -224,7 +216,7 @@
 
 val distinctN = "constr_distinct";
 
-fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
+fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
     FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
       (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
         atac 2, resolve_tac thms 1, etac FalseE 1]))
@@ -248,7 +240,7 @@
          (case (stripT (0, T1), stripT (0, T2)) of
             ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
                 if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
-                   (case (get_datatype_descr thy) tname1 of
+                   (case (get_info_descr thy) tname1 of
                       SOME (_, (_, constrs)) => let val cnames = map fst constrs
                         in if cname1 mem cnames andalso cname2 mem cnames then
                              SOME (distinct_rule thy ss tname1
@@ -273,21 +265,21 @@
 (**** translation rules for case ****)
 
 fun make_case ctxt = DatatypeCase.make_case
-  (datatype_of_constr (ProofContext.theory_of ctxt)) ctxt;
+  (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
 
 fun strip_case ctxt = DatatypeCase.strip_case
-  (datatype_of_case (ProofContext.theory_of ctxt));
+  (info_of_case (ProofContext.theory_of ctxt));
 
 fun add_case_tr' case_names thy =
   Sign.add_advanced_trfuns ([], [],
     map (fn case_name =>
       let val case_name' = Sign.const_syntax_name thy case_name
-      in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
+      in (case_name', DatatypeCase.case_tr' info_of_case case_name')
       end) case_names, []) thy;
 
 val trfun_setup =
   Sign.add_advanced_trfuns ([],
-    [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
+    [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
     [], []);
 
 
@@ -334,15 +326,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 +360,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
@@ -393,16 +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
-    ({distinct = distinct,
-      inject = inject,
-      exhaustion = casedist_thms,
-      rec_thms = rec_thms,
-      case_thms = case_thms,
-      split_thms = split_thms,
-      induction = induct,
-      simps = simps}, thy12)
-  end;
+  in (dt_names, thy12) end;
 
 
 (*********************** declare existing type as datatype *********************)
@@ -420,7 +395,7 @@
       | get_typ t = err t;
     val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
 
-    val dt_info = get_datatypes thy;
+    val dt_info = get_all thy;
 
     val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     val (case_names_induct, case_names_exhausts) =
@@ -457,6 +432,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 +444,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
@@ -499,7 +466,7 @@
 
     val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
     val _ = case map_filter (fn (tyco, _) =>
-        if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
+        if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
      of [] => ()
       | tycos => error ("Type(s) " ^ commas (map quote tycos)
           ^ " already represented inductivly");
@@ -609,7 +576,7 @@
     val (dts', constr_syntax, sorts', i) =
       fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
     val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
-    val dt_info = get_datatypes thy;
+    val dt_info = get_all thy;
     val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
     val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
       if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
@@ -681,7 +648,7 @@
   (fn {source = src, context = ctxt, ...} => fn dtco =>
     let
       val thy = ProofContext.theory_of ctxt;
-      val (vs, cos) = the_datatype_spec thy dtco;
+      val (vs, cos) = the_spec thy dtco;
       val ty = Type (dtco, map TFree vs);
       fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
             Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -276,12 +276,12 @@
 
 fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
    (c as Const (s, T), ts) =>
-     (case Datatype.datatype_of_case thy s of
+     (case Datatype.info_of_case thy s of
         SOME {index, descr, ...} =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           SOME (pretty_case thy defs dep module brack
             (#3 (the (AList.lookup op = descr index))) c ts gr )
-      | NONE => case (Datatype.datatype_of_constr thy s, strip_type T) of
+      | NONE => case (Datatype.info_of_constr thy s, strip_type T) of
         (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           let
@@ -296,7 +296,7 @@
  | _ => NONE);
 
 fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
-      (case Datatype.get_datatype thy s of
+      (case Datatype.get_info thy s of
          NONE => NONE
        | SOME {descr, sorts, ...} =>
            if is_some (get_assoc_type thy s) then NONE else
@@ -331,7 +331,7 @@
 fun mk_case_cert thy tyco =
   let
     val raw_thms =
-      (#case_rewrites o Datatype.the_datatype thy) tyco;
+      (#case_rewrites o Datatype.the_info thy) tyco;
     val thms as hd_thm :: _ = raw_thms
       |> Conjunction.intr_balanced
       |> Thm.unvarify
@@ -364,8 +364,8 @@
 
 fun mk_eq_eqns thy dtco =
   let
-    val (vs, cos) = Datatype.the_datatype_spec thy dtco;
-    val { descr, index, inject = inject_thms, ... } = Datatype.the_datatype thy dtco;
+    val (vs, cos) = Datatype.the_spec thy dtco;
+    val { descr, index, inject = inject_thms, ... } = Datatype.the_info thy dtco;
     val ty = Type (dtco, map TFree vs);
     fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
       $ t1 $ t2;
@@ -428,11 +428,11 @@
 
 fun add_all_code config dtcos thy =
   let
-    val (vs :: _, coss) = (split_list o map (Datatype.the_datatype_spec thy)) dtcos;
+    val (vs :: _, coss) = (split_list o map (Datatype.the_spec thy)) dtcos;
     val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
     val css = if exists is_none any_css then []
       else map_filter I any_css;
-    val case_rewrites = maps (#case_rewrites o Datatype.the_datatype thy) dtcos;
+    val case_rewrites = maps (#case_rewrites o Datatype.the_info thy) dtcos;
     val certs = map (mk_case_cert thy) dtcos;
   in
     if null css then thy
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -217,7 +217,7 @@
   if ! Proofterm.proofs < 2 then thy
   else let
     val _ = message config "Adding realizers for induction and case analysis ..."
-    val infos = map (Datatype.the_datatype thy) names;
+    val infos = map (Datatype.the_info thy) names;
     val info :: _ = infos;
   in
     thy
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/Function/fundef.ML
--- a/src/HOL/Tools/Function/fundef.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/Function/fundef.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -186,7 +186,7 @@
 
 fun add_case_cong n thy =
     Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
-                          (Datatype.get_datatype thy n |> the
+                          (Datatype.the_info thy n
                            |> #case_cong
                            |> safe_mk_meta_eq)))
                        thy
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/Function/fundef_datatype.ML
--- a/src/HOL/Tools/Function/fundef_datatype.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -40,7 +40,7 @@
           let
             val (hd, args) = strip_comb t
           in
-            (((case Datatype.datatype_of_constr thy (fst (dest_Const hd)) of
+            (((case Datatype.info_of_constr thy (fst (dest_Const hd)) of
                  SOME _ => ()
                | NONE => err "Non-constructor pattern")
               handle TERM ("dest_Const", _) => err "Non-constructor patterns");
@@ -103,7 +103,7 @@
 
 fun inst_constrs_of thy (T as Type (name, _)) =
         map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-            (the (Datatype.get_datatype_constrs thy name))
+            (the (Datatype.get_constrs thy name))
   | inst_constrs_of thy _ = raise Match
 
 
@@ -144,7 +144,7 @@
          let
              val T = fastype_of v
              val (tname, _) = dest_Type T
-             val {exhaustion=case_thm, ...} = Datatype.the_datatype thy tname
+             val {exhaustion=case_thm, ...} = Datatype.the_info thy tname
              val constrs = inst_constrs_of thy T
              val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
          in
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -40,7 +40,7 @@
 (* This is copied from "fundef_datatype.ML" *)
 fun inst_constrs_of thy (T as Type (name, _)) =
     map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-        (the (Datatype.get_datatype_constrs thy name))
+        (the (Datatype.get_constrs thy name))
   | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
                             
                             
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -44,14 +44,14 @@
     | SOME t => t);
 
 fun is_poly thy (DtType (name, dts)) =
-      (case Datatype.get_datatype thy name of
+      (case Datatype.get_info thy name of
          NONE => false
        | SOME _ => exists (is_poly thy) dts)
   | is_poly _ _ = true;
 
 fun constrs_of thy name =
   let
-    val {descr, index, ...} = Datatype.the_datatype thy name
+    val {descr, index, ...} = Datatype.the_info thy name
     val SOME (_, _, constrs) = AList.lookup op = descr index
   in constrs end;
 
@@ -220,7 +220,7 @@
 
 fun add_size_thms config (new_type_names as name :: _) thy =
   let
-    val info as {descr, alt_names, ...} = Datatype.the_datatype thy name;
+    val info as {descr, alt_names, ...} = Datatype.the_info thy name;
     val prefix = Long_Name.map_base_name (K (space_implode "_"
       (the_default (map Long_Name.base_name new_type_names) alt_names))) name;
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -88,16 +88,13 @@
      Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
 
 (* get the case_thm (my version) from a type *)
-fun case_thm_of_ty sgn ty  =
+fun case_thm_of_ty thy ty  =
     let
-      val dtypestab = Datatype.get_datatypes sgn;
       val ty_str = case ty of
                      Type(ty_str, _) => ty_str
                    | TFree(s,_)  => error ("Free type: " ^ s)
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
-      val dt = case Symtab.lookup dtypestab ty_str
-                of SOME dt => dt
-                 | NONE => error ("Not a Datatype: " ^ ty_str)
+      val dt = Datatype.the_info thy ty_str
     in
       cases_thm_of_induct_thm (#induction dt)
     end;
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -446,7 +446,7 @@
        slow.*)
      val case_ss = Simplifier.theory_context theory
        (HOL_basic_ss addcongs
-         (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) theory addsimps case_rewrites)
+         (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
      val corollaries' = map (Simplifier.simplify case_ss) corollaries
      val extract = R.CONTEXT_REWRITE_RULE
                      (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/TFL/thry.ML
--- a/src/HOL/Tools/TFL/thry.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/TFL/thry.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -60,20 +60,20 @@
  *---------------------------------------------------------------------------*)
 
 fun match_info thy dtco =
-  case (Datatype.get_datatype thy dtco,
-         Datatype.get_datatype_constrs thy dtco) of
+  case (Datatype.get_info thy dtco,
+         Datatype.get_constrs thy dtco) of
       (SOME { case_name, ... }, SOME constructors) =>
         SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
     | _ => NONE;
 
-fun induct_info thy dtco = case Datatype.get_datatype thy dtco of
+fun induct_info thy dtco = case Datatype.get_info thy dtco of
         NONE => NONE
       | SOME {nchotomy, ...} =>
           SOME {nchotomy = nchotomy,
-                constructors = (map Const o the o Datatype.get_datatype_constrs thy) dtco};
+                constructors = (map Const o the o Datatype.get_constrs thy) dtco};
 
 fun extract_info thy =
- let val infos = (map snd o Symtab.dest o Datatype.get_datatypes) thy
+ let val infos = (map snd o Symtab.dest o Datatype.get_all) thy
  in {case_congs = map (mk_meta_eq o #case_cong) infos,
      case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
  end;
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -101,9 +101,9 @@
 
 fun is_constrt thy =
   let
-    val cnstrs = List.concat (List.concat (map
+    val cnstrs = flat (maps
       (map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd)
-      (Symtab.dest (Datatype.get_datatypes thy))));
+      (Symtab.dest (Datatype.get_all thy)));
     fun check t = (case strip_comb t of
         (Var _, []) => true
       | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -305,16 +305,19 @@
 
     (** datatype representing computational content of inductive set **)
 
-    val ((dummies, dt_info), 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;
-    fun get f = (these oo Option.map) f;
+    val dt_names = these some_dt_names;
+    val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
+    val rec_thms = if null dt_names then []
+      else (#rec_rewrites o Datatype.the_info 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) (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 +327,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 +389,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 +419,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 +478,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;
 
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -246,7 +246,7 @@
 fun gen_primrec_i note def alt_name eqns_atts thy =
   let
     val (eqns, atts) = split_list eqns_atts;
-    val dt_info = Datatype.get_datatypes thy;
+    val dt_info = Datatype.get_all thy;
     val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ;
     val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
     val dts = find_dts dt_info tnames tnames;
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/primrec.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -220,7 +220,7 @@
     val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
       orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
     val tnames = distinct (op =) (map (#1 o snd) eqns);
-    val dts = find_dts (Datatype.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
+    val dts = find_dts (Datatype.get_all (ProofContext.theory_of lthy)) tnames tnames;
     val main_fns = map (fn (tname, {index, ...}) =>
       (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
     val {descr, rec_names, rec_rewrites, ...} =
@@ -239,10 +239,12 @@
     val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
     fun prove lthy defs =
       let
+        val frees = (fold o Term.fold_aterms) (fn Free (x, _) =>
+          if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
         val rewrites = rec_rewrites' @ map (snd o snd) defs;
         fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
         val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
-      in map (fn eq => [Goal.prove lthy [] [] eq tac]) eqs end;
+      in map (fn eq => [Goal.prove lthy frees [] eq tac]) eqs end;
   in ((prefix, (fs, defs)), prove) end
   handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -166,20 +166,19 @@
     val inst = Thm.instantiate_cterm ([(aT, icT)], []);
     fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
     val t_rhs = lambda t_k proto_t_rhs;
-    val eqs0 = [subst_v @{term "0::code_numeral"} eq, subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
+    val eqs0 = [subst_v @{term "0::code_numeral"} eq,
+      subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     val ((_, eqs2), lthy') = Primrec.add_primrec_simple
       [((Binding.name random_aux, T), NoSyn)] eqs1 lthy;
-    val eq_tac = ALLGOALS (simp_tac rew_ss)
-      THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)));
-    val eqs3 = map (fn prop => SkipProof.prove lthy' [v] [] prop (K eq_tac)) eqs0;
     val cT_random_aux = inst pt_random_aux;
     val cT_rhs = inst pt_rhs;
     val rule = @{thm random_aux_rec}
       |> Drule.instantiate ([(aT, icT)],
-           [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)])
-      |> (fn thm => thm OF eqs3);
-    val tac = ALLGOALS (rtac rule);
+           [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
+    val tac = ALLGOALS (rtac rule)
+      THEN ALLGOALS (simp_tac rew_ss)
+      THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
     val simp = SkipProof.prove lthy' [v] [] eq (K tac);
   in (simp, lthy') end;
 
@@ -361,7 +360,7 @@
     val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
     val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
-      Datatype.the_datatype_descr thy raw_tycos;
+      Datatype.the_descr thy raw_tycos;
     val typrep_vs = (map o apsnd)
       (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
     val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -517,7 +517,7 @@
   fun is_IDT_constructor thy (s, T) =
     (case body_type T of
       Type (s', _) =>
-      (case Datatype.get_datatype_constrs thy s' of
+      (case Datatype.get_constrs thy s' of
         SOME constrs =>
         List.exists (fn (cname, cty) =>
           cname = s andalso Sign.typ_instance thy (T, cty)) constrs
@@ -536,7 +536,7 @@
   fun is_IDT_recursor thy (s, T) =
   let
     val rec_names = Symtab.fold (append o #rec_names o snd)
-      (Datatype.get_datatypes thy) []
+      (Datatype.get_all thy) []
   in
     (* I'm not quite sure if checking the name 's' is sufficient, *)
     (* or if we should also check the type 'T'.                   *)
@@ -825,7 +825,7 @@
       (* axiomatic type classes *)
       | Type ("itself", [T1])  => collect_type_axioms (axs, T1)
       | Type (s, Ts)           =>
-        (case Datatype.get_datatype thy s of
+        (case Datatype.get_info thy s of
           SOME info =>  (* inductive datatype *)
             (* only collect relevant type axioms for the argument types *)
             Library.foldl collect_type_axioms (axs, Ts)
@@ -960,7 +960,7 @@
         Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
       | Type ("prop", [])      => acc
       | Type (s, Ts)           =>
-        (case Datatype.get_datatype thy s of
+        (case Datatype.get_info thy s of
           SOME info =>  (* inductive datatype *)
           let
             val index        = #index info
@@ -1172,7 +1172,7 @@
       (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
       val maybe_spurious = Library.exists (fn
           Type (s, _) =>
-          (case Datatype.get_datatype thy s of
+          (case Datatype.get_info thy s of
             SOME info =>  (* inductive datatype *)
             let
               val index           = #index info
@@ -1973,7 +1973,7 @@
     val (typs, terms) = model
     (* Term.typ -> (interpretation * model * arguments) option *)
     fun interpret_term (Type (s, Ts)) =
-      (case Datatype.get_datatype thy s of
+      (case Datatype.get_info thy s of
         SOME info =>  (* inductive datatype *)
         let
           (* int option -- only recursive IDTs have an associated depth *)
@@ -2107,7 +2107,7 @@
             HOLogic_empty_set) pairss
         end
       | Type (s, Ts) =>
-        (case Datatype.get_datatype thy s of
+        (case Datatype.get_info thy s of
           SOME info =>
           (case AList.lookup (op =) typs T of
             SOME 0 =>
@@ -2171,7 +2171,7 @@
         Const (s, T) =>
         (case body_type T of
           Type (s', Ts') =>
-          (case Datatype.get_datatype thy s' of
+          (case Datatype.get_info thy s' of
             SOME info =>  (* body type is an inductive datatype *)
             let
               val index               = #index info
@@ -2652,7 +2652,7 @@
             end
           else
             NONE  (* not a recursion operator of this datatype *)
-        ) (Datatype.get_datatypes thy) NONE
+        ) (Datatype.get_all thy) NONE
     | _ =>  (* head of term is not a constant *)
       NONE;
 
@@ -3201,7 +3201,7 @@
   fun IDT_printer thy model T intr assignment =
     (case T of
       Type (s, Ts) =>
-      (case Datatype.get_datatype thy s of
+      (case Datatype.get_info thy s of
         SOME info =>  (* inductive datatype *)
         let
           val (typs, _)           = model
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Jun 23 21:07:39 2009 +0200
@@ -333,7 +333,7 @@
   let
     val cnstrs = flat (maps
       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
-      (Symtab.dest (Datatype.get_datatypes thy)));
+      (Symtab.dest (Datatype.get_all thy)));
     fun check t = (case strip_comb t of
         (Free _, []) => true
       | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
@@ -875,7 +875,7 @@
 (* else false *)
 fun is_constructor thy t =
   if (is_Type (fastype_of t)) then
-    (case Datatype.get_datatype thy ((fst o dest_Type o fastype_of) t) of
+    (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
       NONE => false
     | SOME info => (let
       val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
@@ -954,7 +954,7 @@
 fun prove_match thy (out_ts : term list) = let
   fun get_case_rewrite t =
     if (is_constructor thy t) then let
-      val case_rewrites = (#case_rewrites (Datatype.the_datatype thy
+      val case_rewrites = (#case_rewrites (Datatype.the_info thy
         ((fst o dest_Type o fastype_of) t)))
       in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
     else []
@@ -1093,7 +1093,7 @@
   fun split_term_tac (Free _) = all_tac
     | split_term_tac t =
       if (is_constructor thy t) then let
-        val info = Datatype.the_datatype thy ((fst o dest_Type o fastype_of) t)
+        val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
         val num_of_constrs = length (#case_rewrites info)
         (* special treatment of pairs -- because of fishing *)
         val split_rules = case (fst o dest_Type o fastype_of) t of
diff -r d78e5cff9a9f -r c8a590599cb5 src/HOLCF/IOA/Modelcheck/MuIOA.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Tue Jun 23 21:05:51 2009 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Tue Jun 23 21:07:39 2009 +0200
@@ -184,7 +184,7 @@
     val subgoal = Thm.term_of csubgoal;
   in
  (let
-    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) sign;
+    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) sign;
     val concl = Logic.strip_imp_concl subgoal;
     val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
     val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));