merged
authorhaftmann
Tue Jun 23 21:07:39 2009 +0200 (2009-06-23)
changeset 31789c8a590599cb5
parent 31780 d78e5cff9a9f
parent 31788 496c86f5f9e9
child 31790 05c92381363c
merged
     1.1 --- a/NEWS	Tue Jun 23 21:05:51 2009 +0200
     1.2 +++ b/NEWS	Tue Jun 23 21:07:39 2009 +0200
     1.3 @@ -52,10 +52,12 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -
     1.8  * NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
     1.9  If possible, use NewNumberTheory, not NumberTheory.
    1.10  
    1.11 +* Simplified interfaces of datatype module.  INCOMPATIBILITY.
    1.12 +
    1.13 +
    1.14  *** ML ***
    1.15  
    1.16  * Eliminated old Attrib.add_attributes, Method.add_methods and related
     2.1 --- a/src/HOL/Inductive.thy	Tue Jun 23 21:05:51 2009 +0200
     2.2 +++ b/src/HOL/Inductive.thy	Tue Jun 23 21:07:39 2009 +0200
     2.3 @@ -364,7 +364,7 @@
     2.4    fun fun_tr ctxt [cs] =
     2.5      let
     2.6        val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
     2.7 -      val ft = DatatypeCase.case_tr true Datatype.datatype_of_constr
     2.8 +      val ft = DatatypeCase.case_tr true Datatype.info_of_constr
     2.9                   ctxt [x, cs]
    2.10      in lambda x ft end
    2.11  in [("_lam_pats_syntax", fun_tr)] end
     3.1 --- a/src/HOL/List.thy	Tue Jun 23 21:05:51 2009 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Jun 23 21:07:39 2009 +0200
     3.3 @@ -363,7 +363,7 @@
     3.4        val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
     3.5                                          $ NilC;
     3.6        val cs = Syntax.const "_case2" $ case1 $ case2
     3.7 -      val ft = DatatypeCase.case_tr false Datatype.datatype_of_constr
     3.8 +      val ft = DatatypeCase.case_tr false Datatype.info_of_constr
     3.9                   ctxt [x, cs]
    3.10      in lambda x ft end;
    3.11  
     4.1 --- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 21:05:51 2009 +0200
     4.2 +++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 21:07:39 2009 +0200
     4.3 @@ -241,13 +241,12 @@
     4.4          map replace_types cargs, NoSyn)) constrs)) dts';
     4.5  
     4.6      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     4.7 -    val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
     4.8  
     4.9 -    val ({induction, ...},thy1) =
    4.10 +    val (full_new_type_names',thy1) =
    4.11        Datatype.add_datatype config new_type_names' dts'' thy;
    4.12  
    4.13 -    val SOME {descr, ...} = Symtab.lookup
    4.14 -      (Datatype.get_datatypes thy1) (hd full_new_type_names');
    4.15 +    val {descr, induction, ...} =
    4.16 +      Datatype.the_info thy1 (hd full_new_type_names');
    4.17      fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
    4.18  
    4.19      val big_name = space_implode "_" new_type_names;
     5.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 21:05:51 2009 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jun 23 21:07:39 2009 +0200
     5.3 @@ -101,9 +101,10 @@
     5.4      val (_,thy1) = 
     5.5      fold_map (fn ak => fn thy => 
     5.6            let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
     5.7 -              val ({inject,case_thms,...},thy1) = Datatype.add_datatype
     5.8 -                Datatype.default_config [ak] [dt] thy
     5.9 -              val inject_flat = flat inject
    5.10 +              val (dt_names, thy1) = Datatype.add_datatype
    5.11 +                Datatype.default_config [ak] [dt] thy;
    5.12 +            
    5.13 +              val injects = maps (#inject o Datatype.the_info thy1) dt_names;
    5.14                val ak_type = Type (Sign.intern_type thy1 ak,[])
    5.15                val ak_sign = Sign.intern_const thy1 ak 
    5.16                
    5.17 @@ -115,7 +116,7 @@
    5.18                    (Const (@{const_name "inj_on"},inj_on_type) $ 
    5.19                           Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat})
    5.20  
    5.21 -              val simp1 = @{thm inj_on_def}::inject_flat
    5.22 +              val simp1 = @{thm inj_on_def} :: injects;
    5.23                
    5.24                val proof1 = fn _ => EVERY [simp_tac (HOL_basic_ss addsimps simp1) 1,
    5.25                                            rtac @{thm ballI} 1,
     6.1 --- a/src/HOL/Statespace/state_fun.ML	Tue Jun 23 21:05:51 2009 +0200
     6.2 +++ b/src/HOL/Statespace/state_fun.ML	Tue Jun 23 21:07:39 2009 +0200
     6.3 @@ -340,7 +340,7 @@
     6.4    | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
     6.5    | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
     6.6  
     6.7 -fun is_datatype thy n = is_some (Symtab.lookup (Datatype.get_datatypes thy) n);
     6.8 +fun is_datatype thy = is_some o Datatype.get_info thy;
     6.9  
    6.10  fun mk_map "List.list" = Syntax.const "List.map"
    6.11    | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
     7.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 21:05:51 2009 +0200
     7.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 21:07:39 2009 +0200
     7.3 @@ -7,31 +7,23 @@
     7.4  signature DATATYPE =
     7.5  sig
     7.6    include DATATYPE_COMMON
     7.7 -  type rules = {distinct : thm list list,
     7.8 -    inject : thm list list,
     7.9 -    exhaustion : thm list,
    7.10 -    rec_thms : thm list,
    7.11 -    case_thms : thm list list,
    7.12 -    split_thms : (thm * thm) list,
    7.13 -    induction : thm,
    7.14 -    simps : thm list}
    7.15    val add_datatype : config -> string list -> (string list * binding * mixfix *
    7.16 -    (binding * typ list * mixfix) list) list -> theory -> rules * theory
    7.17 +    (binding * typ list * mixfix) list) list -> theory -> string list * theory
    7.18    val datatype_cmd : string list -> (string list * binding * mixfix *
    7.19      (binding * string list * mixfix) list) list -> theory -> theory
    7.20 -  val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
    7.21 +  val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    7.22      -> string list option -> term list -> theory -> Proof.state
    7.23    val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
    7.24 -  val get_datatypes : theory -> info Symtab.table
    7.25 -  val get_datatype : theory -> string -> info option
    7.26 -  val the_datatype : theory -> string -> info
    7.27 -  val datatype_of_constr : theory -> string -> info option
    7.28 -  val datatype_of_case : theory -> string -> info option
    7.29 -  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
    7.30 -  val the_datatype_descr : theory -> string list
    7.31 +  val get_info : theory -> string -> info option
    7.32 +  val the_info : theory -> string -> info
    7.33 +  val the_descr : theory -> string list
    7.34      -> descr * (string * sort) list * string list
    7.35        * (string list * string list) * (typ list * typ list)
    7.36 -  val get_datatype_constrs : theory -> string -> (string * typ) list option
    7.37 +  val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
    7.38 +  val get_constrs : theory -> string -> (string * typ) list option
    7.39 +  val get_all : theory -> info Symtab.table
    7.40 +  val info_of_constr : theory -> string -> info option
    7.41 +  val info_of_case : theory -> string -> info option
    7.42    val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
    7.43    val distinct_simproc : simproc
    7.44    val make_case :  Proof.context -> bool -> string list -> term ->
    7.45 @@ -69,7 +61,7 @@
    7.46       cases = Symtab.merge (K true) (cases1, cases2)};
    7.47  );
    7.48  
    7.49 -val get_datatypes = #types o DatatypesData.get;
    7.50 +val get_all = #types o DatatypesData.get;
    7.51  val map_datatypes = DatatypesData.map;
    7.52  
    7.53  
    7.54 @@ -85,23 +77,23 @@
    7.55         (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
    7.56         cases});
    7.57  
    7.58 -val get_datatype = Symtab.lookup o get_datatypes;
    7.59 +val get_info = Symtab.lookup o get_all;
    7.60  
    7.61 -fun the_datatype thy name = (case get_datatype thy name of
    7.62 +fun the_info thy name = (case get_info thy name of
    7.63        SOME info => info
    7.64      | NONE => error ("Unknown datatype " ^ quote name));
    7.65  
    7.66 -val datatype_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
    7.67 -val datatype_of_case = Symtab.lookup o #cases o DatatypesData.get;
    7.68 +val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
    7.69 +val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
    7.70  
    7.71 -fun get_datatype_descr thy dtco =
    7.72 -  get_datatype thy dtco
    7.73 +fun get_info_descr thy dtco =
    7.74 +  get_info thy dtco
    7.75    |> Option.map (fn info as { descr, index, ... } =>
    7.76         (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
    7.77  
    7.78 -fun the_datatype_spec thy dtco =
    7.79 +fun the_spec thy dtco =
    7.80    let
    7.81 -    val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
    7.82 +    val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
    7.83      val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
    7.84      val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
    7.85        o DatatypeAux.dest_DtTFree) dtys;
    7.86 @@ -109,9 +101,9 @@
    7.87        (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
    7.88    in (sorts, cos) end;
    7.89  
    7.90 -fun the_datatype_descr thy (raw_tycos as raw_tyco :: _) =
    7.91 +fun the_descr thy (raw_tycos as raw_tyco :: _) =
    7.92    let
    7.93 -    val info = the_datatype thy raw_tyco;
    7.94 +    val info = the_info thy raw_tyco;
    7.95      val descr = #descr info;
    7.96  
    7.97      val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
    7.98 @@ -137,8 +129,8 @@
    7.99  
   7.100    in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
   7.101  
   7.102 -fun get_datatype_constrs thy dtco =
   7.103 -  case try (the_datatype_spec thy) dtco
   7.104 +fun get_constrs thy dtco =
   7.105 +  case try (the_spec thy) dtco
   7.106     of SOME (sorts, cos) =>
   7.107          let
   7.108            fun subst (v, sort) = TVar ((v, 0), sort);
   7.109 @@ -224,7 +216,7 @@
   7.110  
   7.111  val distinctN = "constr_distinct";
   7.112  
   7.113 -fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
   7.114 +fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
   7.115      FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
   7.116        (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
   7.117          atac 2, resolve_tac thms 1, etac FalseE 1]))
   7.118 @@ -248,7 +240,7 @@
   7.119           (case (stripT (0, T1), stripT (0, T2)) of
   7.120              ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
   7.121                  if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
   7.122 -                   (case (get_datatype_descr thy) tname1 of
   7.123 +                   (case (get_info_descr thy) tname1 of
   7.124                        SOME (_, (_, constrs)) => let val cnames = map fst constrs
   7.125                          in if cname1 mem cnames andalso cname2 mem cnames then
   7.126                               SOME (distinct_rule thy ss tname1
   7.127 @@ -273,21 +265,21 @@
   7.128  (**** translation rules for case ****)
   7.129  
   7.130  fun make_case ctxt = DatatypeCase.make_case
   7.131 -  (datatype_of_constr (ProofContext.theory_of ctxt)) ctxt;
   7.132 +  (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
   7.133  
   7.134  fun strip_case ctxt = DatatypeCase.strip_case
   7.135 -  (datatype_of_case (ProofContext.theory_of ctxt));
   7.136 +  (info_of_case (ProofContext.theory_of ctxt));
   7.137  
   7.138  fun add_case_tr' case_names thy =
   7.139    Sign.add_advanced_trfuns ([], [],
   7.140      map (fn case_name =>
   7.141        let val case_name' = Sign.const_syntax_name thy case_name
   7.142 -      in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
   7.143 +      in (case_name', DatatypeCase.case_tr' info_of_case case_name')
   7.144        end) case_names, []) thy;
   7.145  
   7.146  val trfun_setup =
   7.147    Sign.add_advanced_trfuns ([],
   7.148 -    [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
   7.149 +    [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
   7.150      [], []);
   7.151  
   7.152  
   7.153 @@ -334,15 +326,6 @@
   7.154      case_cong = case_cong,
   7.155      weak_case_cong = weak_case_cong});
   7.156  
   7.157 -type rules = {distinct : thm list list,
   7.158 -  inject : thm list list,
   7.159 -  exhaustion : thm list,
   7.160 -  rec_thms : thm list,
   7.161 -  case_thms : thm list list,
   7.162 -  split_thms : (thm * thm) list,
   7.163 -  induction : thm,
   7.164 -  simps : thm list}
   7.165 -
   7.166  structure DatatypeInterpretation = InterpretationFun
   7.167    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
   7.168  fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
   7.169 @@ -377,10 +360,11 @@
   7.170  
   7.171      val dt_infos = map
   7.172        (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
   7.173 -      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   7.174 +      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
   7.175          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   7.176  
   7.177      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   7.178 +    val dt_names = map fst dt_infos;
   7.179  
   7.180      val thy12 =
   7.181        thy10
   7.182 @@ -393,16 +377,7 @@
   7.183        |> Sign.parent_path
   7.184        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   7.185        |> DatatypeInterpretation.data (config, map fst dt_infos);
   7.186 -  in
   7.187 -    ({distinct = distinct,
   7.188 -      inject = inject,
   7.189 -      exhaustion = casedist_thms,
   7.190 -      rec_thms = rec_thms,
   7.191 -      case_thms = case_thms,
   7.192 -      split_thms = split_thms,
   7.193 -      induction = induct,
   7.194 -      simps = simps}, thy12)
   7.195 -  end;
   7.196 +  in (dt_names, thy12) end;
   7.197  
   7.198  
   7.199  (*********************** declare existing type as datatype *********************)
   7.200 @@ -420,7 +395,7 @@
   7.201        | get_typ t = err t;
   7.202      val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
   7.203  
   7.204 -    val dt_info = get_datatypes thy;
   7.205 +    val dt_info = get_all thy;
   7.206  
   7.207      val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
   7.208      val (case_names_induct, case_names_exhausts) =
   7.209 @@ -457,6 +432,7 @@
   7.210          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   7.211  
   7.212      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   7.213 +    val dt_names = map fst dt_infos;
   7.214  
   7.215      val thy11 =
   7.216        thy10
   7.217 @@ -468,17 +444,8 @@
   7.218        |> Sign.parent_path
   7.219        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   7.220        |> snd
   7.221 -      |> DatatypeInterpretation.data (config, map fst dt_infos);
   7.222 -  in
   7.223 -    ({distinct = distinct,
   7.224 -      inject = inject,
   7.225 -      exhaustion = casedist_thms,
   7.226 -      rec_thms = rec_thms,
   7.227 -      case_thms = case_thms,
   7.228 -      split_thms = split_thms,
   7.229 -      induction = induct',
   7.230 -      simps = simps}, thy11)
   7.231 -  end;
   7.232 +      |> DatatypeInterpretation.data (config, dt_names);
   7.233 +  in (dt_names, thy11) end;
   7.234  
   7.235  fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
   7.236    let
   7.237 @@ -499,7 +466,7 @@
   7.238  
   7.239      val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
   7.240      val _ = case map_filter (fn (tyco, _) =>
   7.241 -        if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
   7.242 +        if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
   7.243       of [] => ()
   7.244        | tycos => error ("Type(s) " ^ commas (map quote tycos)
   7.245            ^ " already represented inductivly");
   7.246 @@ -609,7 +576,7 @@
   7.247      val (dts', constr_syntax, sorts', i) =
   7.248        fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
   7.249      val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
   7.250 -    val dt_info = get_datatypes thy;
   7.251 +    val dt_info = get_all thy;
   7.252      val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   7.253      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   7.254        if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   7.255 @@ -681,7 +648,7 @@
   7.256    (fn {source = src, context = ctxt, ...} => fn dtco =>
   7.257      let
   7.258        val thy = ProofContext.theory_of ctxt;
   7.259 -      val (vs, cos) = the_datatype_spec thy dtco;
   7.260 +      val (vs, cos) = the_spec thy dtco;
   7.261        val ty = Type (dtco, map TFree vs);
   7.262        fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
   7.263              Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
     8.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Jun 23 21:05:51 2009 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Jun 23 21:07:39 2009 +0200
     8.3 @@ -276,12 +276,12 @@
     8.4  
     8.5  fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
     8.6     (c as Const (s, T), ts) =>
     8.7 -     (case Datatype.datatype_of_case thy s of
     8.8 +     (case Datatype.info_of_case thy s of
     8.9          SOME {index, descr, ...} =>
    8.10            if is_some (get_assoc_code thy (s, T)) then NONE else
    8.11            SOME (pretty_case thy defs dep module brack
    8.12              (#3 (the (AList.lookup op = descr index))) c ts gr )
    8.13 -      | NONE => case (Datatype.datatype_of_constr thy s, strip_type T) of
    8.14 +      | NONE => case (Datatype.info_of_constr thy s, strip_type T) of
    8.15          (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
    8.16            if is_some (get_assoc_code thy (s, T)) then NONE else
    8.17            let
    8.18 @@ -296,7 +296,7 @@
    8.19   | _ => NONE);
    8.20  
    8.21  fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
    8.22 -      (case Datatype.get_datatype thy s of
    8.23 +      (case Datatype.get_info thy s of
    8.24           NONE => NONE
    8.25         | SOME {descr, sorts, ...} =>
    8.26             if is_some (get_assoc_type thy s) then NONE else
    8.27 @@ -331,7 +331,7 @@
    8.28  fun mk_case_cert thy tyco =
    8.29    let
    8.30      val raw_thms =
    8.31 -      (#case_rewrites o Datatype.the_datatype thy) tyco;
    8.32 +      (#case_rewrites o Datatype.the_info thy) tyco;
    8.33      val thms as hd_thm :: _ = raw_thms
    8.34        |> Conjunction.intr_balanced
    8.35        |> Thm.unvarify
    8.36 @@ -364,8 +364,8 @@
    8.37  
    8.38  fun mk_eq_eqns thy dtco =
    8.39    let
    8.40 -    val (vs, cos) = Datatype.the_datatype_spec thy dtco;
    8.41 -    val { descr, index, inject = inject_thms, ... } = Datatype.the_datatype thy dtco;
    8.42 +    val (vs, cos) = Datatype.the_spec thy dtco;
    8.43 +    val { descr, index, inject = inject_thms, ... } = Datatype.the_info thy dtco;
    8.44      val ty = Type (dtco, map TFree vs);
    8.45      fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
    8.46        $ t1 $ t2;
    8.47 @@ -428,11 +428,11 @@
    8.48  
    8.49  fun add_all_code config dtcos thy =
    8.50    let
    8.51 -    val (vs :: _, coss) = (split_list o map (Datatype.the_datatype_spec thy)) dtcos;
    8.52 +    val (vs :: _, coss) = (split_list o map (Datatype.the_spec thy)) dtcos;
    8.53      val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
    8.54      val css = if exists is_none any_css then []
    8.55        else map_filter I any_css;
    8.56 -    val case_rewrites = maps (#case_rewrites o Datatype.the_datatype thy) dtcos;
    8.57 +    val case_rewrites = maps (#case_rewrites o Datatype.the_info thy) dtcos;
    8.58      val certs = map (mk_case_cert thy) dtcos;
    8.59    in
    8.60      if null css then thy
     9.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 23 21:05:51 2009 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 23 21:07:39 2009 +0200
     9.3 @@ -217,7 +217,7 @@
     9.4    if ! Proofterm.proofs < 2 then thy
     9.5    else let
     9.6      val _ = message config "Adding realizers for induction and case analysis ..."
     9.7 -    val infos = map (Datatype.the_datatype thy) names;
     9.8 +    val infos = map (Datatype.the_info thy) names;
     9.9      val info :: _ = infos;
    9.10    in
    9.11      thy
    10.1 --- a/src/HOL/Tools/Function/fundef.ML	Tue Jun 23 21:05:51 2009 +0200
    10.2 +++ b/src/HOL/Tools/Function/fundef.ML	Tue Jun 23 21:07:39 2009 +0200
    10.3 @@ -186,7 +186,7 @@
    10.4  
    10.5  fun add_case_cong n thy =
    10.6      Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
    10.7 -                          (Datatype.get_datatype thy n |> the
    10.8 +                          (Datatype.the_info thy n
    10.9                             |> #case_cong
   10.10                             |> safe_mk_meta_eq)))
   10.11                         thy
    11.1 --- a/src/HOL/Tools/Function/fundef_datatype.ML	Tue Jun 23 21:05:51 2009 +0200
    11.2 +++ b/src/HOL/Tools/Function/fundef_datatype.ML	Tue Jun 23 21:07:39 2009 +0200
    11.3 @@ -40,7 +40,7 @@
    11.4            let
    11.5              val (hd, args) = strip_comb t
    11.6            in
    11.7 -            (((case Datatype.datatype_of_constr thy (fst (dest_Const hd)) of
    11.8 +            (((case Datatype.info_of_constr thy (fst (dest_Const hd)) of
    11.9                   SOME _ => ()
   11.10                 | NONE => err "Non-constructor pattern")
   11.11                handle TERM ("dest_Const", _) => err "Non-constructor patterns");
   11.12 @@ -103,7 +103,7 @@
   11.13  
   11.14  fun inst_constrs_of thy (T as Type (name, _)) =
   11.15          map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
   11.16 -            (the (Datatype.get_datatype_constrs thy name))
   11.17 +            (the (Datatype.get_constrs thy name))
   11.18    | inst_constrs_of thy _ = raise Match
   11.19  
   11.20  
   11.21 @@ -144,7 +144,7 @@
   11.22           let
   11.23               val T = fastype_of v
   11.24               val (tname, _) = dest_Type T
   11.25 -             val {exhaustion=case_thm, ...} = Datatype.the_datatype thy tname
   11.26 +             val {exhaustion=case_thm, ...} = Datatype.the_info thy tname
   11.27               val constrs = inst_constrs_of thy T
   11.28               val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
   11.29           in
    12.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Tue Jun 23 21:05:51 2009 +0200
    12.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Tue Jun 23 21:07:39 2009 +0200
    12.3 @@ -40,7 +40,7 @@
    12.4  (* This is copied from "fundef_datatype.ML" *)
    12.5  fun inst_constrs_of thy (T as Type (name, _)) =
    12.6      map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    12.7 -        (the (Datatype.get_datatype_constrs thy name))
    12.8 +        (the (Datatype.get_constrs thy name))
    12.9    | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
   12.10                              
   12.11                              
    13.1 --- a/src/HOL/Tools/Function/size.ML	Tue Jun 23 21:05:51 2009 +0200
    13.2 +++ b/src/HOL/Tools/Function/size.ML	Tue Jun 23 21:07:39 2009 +0200
    13.3 @@ -44,14 +44,14 @@
    13.4      | SOME t => t);
    13.5  
    13.6  fun is_poly thy (DtType (name, dts)) =
    13.7 -      (case Datatype.get_datatype thy name of
    13.8 +      (case Datatype.get_info thy name of
    13.9           NONE => false
   13.10         | SOME _ => exists (is_poly thy) dts)
   13.11    | is_poly _ _ = true;
   13.12  
   13.13  fun constrs_of thy name =
   13.14    let
   13.15 -    val {descr, index, ...} = Datatype.the_datatype thy name
   13.16 +    val {descr, index, ...} = Datatype.the_info thy name
   13.17      val SOME (_, _, constrs) = AList.lookup op = descr index
   13.18    in constrs end;
   13.19  
   13.20 @@ -220,7 +220,7 @@
   13.21  
   13.22  fun add_size_thms config (new_type_names as name :: _) thy =
   13.23    let
   13.24 -    val info as {descr, alt_names, ...} = Datatype.the_datatype thy name;
   13.25 +    val info as {descr, alt_names, ...} = Datatype.the_info thy name;
   13.26      val prefix = Long_Name.map_base_name (K (space_implode "_"
   13.27        (the_default (map Long_Name.base_name new_type_names) alt_names))) name;
   13.28      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
    14.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Tue Jun 23 21:05:51 2009 +0200
    14.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Tue Jun 23 21:07:39 2009 +0200
    14.3 @@ -88,16 +88,13 @@
    14.4       Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
    14.5  
    14.6  (* get the case_thm (my version) from a type *)
    14.7 -fun case_thm_of_ty sgn ty  =
    14.8 +fun case_thm_of_ty thy ty  =
    14.9      let
   14.10 -      val dtypestab = Datatype.get_datatypes sgn;
   14.11        val ty_str = case ty of
   14.12                       Type(ty_str, _) => ty_str
   14.13                     | TFree(s,_)  => error ("Free type: " ^ s)
   14.14                     | TVar((s,i),_) => error ("Free variable: " ^ s)
   14.15 -      val dt = case Symtab.lookup dtypestab ty_str
   14.16 -                of SOME dt => dt
   14.17 -                 | NONE => error ("Not a Datatype: " ^ ty_str)
   14.18 +      val dt = Datatype.the_info thy ty_str
   14.19      in
   14.20        cases_thm_of_induct_thm (#induction dt)
   14.21      end;
    15.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Jun 23 21:05:51 2009 +0200
    15.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Jun 23 21:07:39 2009 +0200
    15.3 @@ -446,7 +446,7 @@
    15.4         slow.*)
    15.5       val case_ss = Simplifier.theory_context theory
    15.6         (HOL_basic_ss addcongs
    15.7 -         (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) theory addsimps case_rewrites)
    15.8 +         (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
    15.9       val corollaries' = map (Simplifier.simplify case_ss) corollaries
   15.10       val extract = R.CONTEXT_REWRITE_RULE
   15.11                       (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)
    16.1 --- a/src/HOL/Tools/TFL/thry.ML	Tue Jun 23 21:05:51 2009 +0200
    16.2 +++ b/src/HOL/Tools/TFL/thry.ML	Tue Jun 23 21:07:39 2009 +0200
    16.3 @@ -60,20 +60,20 @@
    16.4   *---------------------------------------------------------------------------*)
    16.5  
    16.6  fun match_info thy dtco =
    16.7 -  case (Datatype.get_datatype thy dtco,
    16.8 -         Datatype.get_datatype_constrs thy dtco) of
    16.9 +  case (Datatype.get_info thy dtco,
   16.10 +         Datatype.get_constrs thy dtco) of
   16.11        (SOME { case_name, ... }, SOME constructors) =>
   16.12          SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
   16.13      | _ => NONE;
   16.14  
   16.15 -fun induct_info thy dtco = case Datatype.get_datatype thy dtco of
   16.16 +fun induct_info thy dtco = case Datatype.get_info thy dtco of
   16.17          NONE => NONE
   16.18        | SOME {nchotomy, ...} =>
   16.19            SOME {nchotomy = nchotomy,
   16.20 -                constructors = (map Const o the o Datatype.get_datatype_constrs thy) dtco};
   16.21 +                constructors = (map Const o the o Datatype.get_constrs thy) dtco};
   16.22  
   16.23  fun extract_info thy =
   16.24 - let val infos = (map snd o Symtab.dest o Datatype.get_datatypes) thy
   16.25 + let val infos = (map snd o Symtab.dest o Datatype.get_all) thy
   16.26   in {case_congs = map (mk_meta_eq o #case_cong) infos,
   16.27       case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
   16.28   end;
    17.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Jun 23 21:05:51 2009 +0200
    17.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jun 23 21:07:39 2009 +0200
    17.3 @@ -101,9 +101,9 @@
    17.4  
    17.5  fun is_constrt thy =
    17.6    let
    17.7 -    val cnstrs = List.concat (List.concat (map
    17.8 +    val cnstrs = flat (maps
    17.9        (map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd)
   17.10 -      (Symtab.dest (Datatype.get_datatypes thy))));
   17.11 +      (Symtab.dest (Datatype.get_all thy)));
   17.12      fun check t = (case strip_comb t of
   17.13          (Var _, []) => true
   17.14        | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
    18.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 21:05:51 2009 +0200
    18.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 23 21:07:39 2009 +0200
    18.3 @@ -305,16 +305,19 @@
    18.4  
    18.5      (** datatype representing computational content of inductive set **)
    18.6  
    18.7 -    val ((dummies, dt_info), thy2) =
    18.8 +    val ((dummies, some_dt_names), thy2) =
    18.9        thy1
   18.10        |> add_dummies (Datatype.add_datatype
   18.11             { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
   18.12             (map (pair false) dts) []
   18.13        ||> Extraction.add_typeof_eqns_i ty_eqs
   18.14        ||> Extraction.add_realizes_eqns_i rlz_eqs;
   18.15 -    fun get f = (these oo Option.map) f;
   18.16 +    val dt_names = these some_dt_names;
   18.17 +    val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
   18.18 +    val rec_thms = if null dt_names then []
   18.19 +      else (#rec_rewrites o Datatype.the_info thy2) (hd dt_names);
   18.20      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
   18.21 -      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
   18.22 +      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
   18.23      val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
   18.24        if member (op =) rsets s then
   18.25          let
   18.26 @@ -324,7 +327,7 @@
   18.27            HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
   18.28          end
   18.29        else (replicate (length rs) Extraction.nullt, (recs, dummies)))
   18.30 -        rss (get #rec_thms dt_info, dummies);
   18.31 +        rss (rec_thms, dummies);
   18.32      val rintrs = map (fn (intr, c) => Envir.eta_contract
   18.33        (Extraction.realizes_of thy2 vs
   18.34          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   18.35 @@ -386,8 +389,7 @@
   18.36            end) (rlzs ~~ rnames);
   18.37          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   18.38            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
   18.39 -        val rews = map mk_meta_eq
   18.40 -          (fst_conv :: snd_conv :: get #rec_thms dt_info);
   18.41 +        val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
   18.42          val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
   18.43            [rtac (#raw_induct ind_info) 1,
   18.44             rewrite_goals_tac rews,
   18.45 @@ -417,7 +419,7 @@
   18.46      (** realizer for elimination rules **)
   18.47  
   18.48      val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
   18.49 -      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
   18.50 +      HOLogic.dest_Trueprop o prop_of o hd) case_thms;
   18.51  
   18.52      fun add_elim_realizer Ps
   18.53        (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
   18.54 @@ -476,7 +478,7 @@
   18.55      val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
   18.56        add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
   18.57          (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   18.58 -           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
   18.59 +           elimps ~~ case_thms ~~ case_names ~~ dummies)
   18.60  
   18.61    in Sign.restore_naming thy thy6 end;
   18.62  
    19.1 --- a/src/HOL/Tools/old_primrec.ML	Tue Jun 23 21:05:51 2009 +0200
    19.2 +++ b/src/HOL/Tools/old_primrec.ML	Tue Jun 23 21:07:39 2009 +0200
    19.3 @@ -246,7 +246,7 @@
    19.4  fun gen_primrec_i note def alt_name eqns_atts thy =
    19.5    let
    19.6      val (eqns, atts) = split_list eqns_atts;
    19.7 -    val dt_info = Datatype.get_datatypes thy;
    19.8 +    val dt_info = Datatype.get_all thy;
    19.9      val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ;
   19.10      val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
   19.11      val dts = find_dts dt_info tnames tnames;
    20.1 --- a/src/HOL/Tools/primrec.ML	Tue Jun 23 21:05:51 2009 +0200
    20.2 +++ b/src/HOL/Tools/primrec.ML	Tue Jun 23 21:07:39 2009 +0200
    20.3 @@ -220,7 +220,7 @@
    20.4      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
    20.5        orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
    20.6      val tnames = distinct (op =) (map (#1 o snd) eqns);
    20.7 -    val dts = find_dts (Datatype.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
    20.8 +    val dts = find_dts (Datatype.get_all (ProofContext.theory_of lthy)) tnames tnames;
    20.9      val main_fns = map (fn (tname, {index, ...}) =>
   20.10        (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
   20.11      val {descr, rec_names, rec_rewrites, ...} =
   20.12 @@ -239,10 +239,12 @@
   20.13      val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
   20.14      fun prove lthy defs =
   20.15        let
   20.16 +        val frees = (fold o Term.fold_aterms) (fn Free (x, _) =>
   20.17 +          if Variable.is_fixed lthy x then I else insert (op =) x | _ => I) eqs [];
   20.18          val rewrites = rec_rewrites' @ map (snd o snd) defs;
   20.19          fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
   20.20          val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
   20.21 -      in map (fn eq => [Goal.prove lthy [] [] eq tac]) eqs end;
   20.22 +      in map (fn eq => [Goal.prove lthy frees [] eq tac]) eqs end;
   20.23    in ((prefix, (fs, defs)), prove) end
   20.24    handle PrimrecError (msg, some_eqn) =>
   20.25      error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
    21.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 23 21:05:51 2009 +0200
    21.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 23 21:07:39 2009 +0200
    21.3 @@ -166,20 +166,19 @@
    21.4      val inst = Thm.instantiate_cterm ([(aT, icT)], []);
    21.5      fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
    21.6      val t_rhs = lambda t_k proto_t_rhs;
    21.7 -    val eqs0 = [subst_v @{term "0::code_numeral"} eq, subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
    21.8 +    val eqs0 = [subst_v @{term "0::code_numeral"} eq,
    21.9 +      subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
   21.10      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
   21.11      val ((_, eqs2), lthy') = Primrec.add_primrec_simple
   21.12        [((Binding.name random_aux, T), NoSyn)] eqs1 lthy;
   21.13 -    val eq_tac = ALLGOALS (simp_tac rew_ss)
   21.14 -      THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)));
   21.15 -    val eqs3 = map (fn prop => SkipProof.prove lthy' [v] [] prop (K eq_tac)) eqs0;
   21.16      val cT_random_aux = inst pt_random_aux;
   21.17      val cT_rhs = inst pt_rhs;
   21.18      val rule = @{thm random_aux_rec}
   21.19        |> Drule.instantiate ([(aT, icT)],
   21.20 -           [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)])
   21.21 -      |> (fn thm => thm OF eqs3);
   21.22 -    val tac = ALLGOALS (rtac rule);
   21.23 +           [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
   21.24 +    val tac = ALLGOALS (rtac rule)
   21.25 +      THEN ALLGOALS (simp_tac rew_ss)
   21.26 +      THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
   21.27      val simp = SkipProof.prove lthy' [v] [] eq (K tac);
   21.28    in (simp, lthy') end;
   21.29  
   21.30 @@ -361,7 +360,7 @@
   21.31      val pp = Syntax.pp_global thy;
   21.32      val algebra = Sign.classes_of thy;
   21.33      val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
   21.34 -      Datatype.the_datatype_descr thy raw_tycos;
   21.35 +      Datatype.the_descr thy raw_tycos;
   21.36      val typrep_vs = (map o apsnd)
   21.37        (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
   21.38      val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
    22.1 --- a/src/HOL/Tools/refute.ML	Tue Jun 23 21:05:51 2009 +0200
    22.2 +++ b/src/HOL/Tools/refute.ML	Tue Jun 23 21:07:39 2009 +0200
    22.3 @@ -517,7 +517,7 @@
    22.4    fun is_IDT_constructor thy (s, T) =
    22.5      (case body_type T of
    22.6        Type (s', _) =>
    22.7 -      (case Datatype.get_datatype_constrs thy s' of
    22.8 +      (case Datatype.get_constrs thy s' of
    22.9          SOME constrs =>
   22.10          List.exists (fn (cname, cty) =>
   22.11            cname = s andalso Sign.typ_instance thy (T, cty)) constrs
   22.12 @@ -536,7 +536,7 @@
   22.13    fun is_IDT_recursor thy (s, T) =
   22.14    let
   22.15      val rec_names = Symtab.fold (append o #rec_names o snd)
   22.16 -      (Datatype.get_datatypes thy) []
   22.17 +      (Datatype.get_all thy) []
   22.18    in
   22.19      (* I'm not quite sure if checking the name 's' is sufficient, *)
   22.20      (* or if we should also check the type 'T'.                   *)
   22.21 @@ -825,7 +825,7 @@
   22.22        (* axiomatic type classes *)
   22.23        | Type ("itself", [T1])  => collect_type_axioms (axs, T1)
   22.24        | Type (s, Ts)           =>
   22.25 -        (case Datatype.get_datatype thy s of
   22.26 +        (case Datatype.get_info thy s of
   22.27            SOME info =>  (* inductive datatype *)
   22.28              (* only collect relevant type axioms for the argument types *)
   22.29              Library.foldl collect_type_axioms (axs, Ts)
   22.30 @@ -960,7 +960,7 @@
   22.31          Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
   22.32        | Type ("prop", [])      => acc
   22.33        | Type (s, Ts)           =>
   22.34 -        (case Datatype.get_datatype thy s of
   22.35 +        (case Datatype.get_info thy s of
   22.36            SOME info =>  (* inductive datatype *)
   22.37            let
   22.38              val index        = #index info
   22.39 @@ -1172,7 +1172,7 @@
   22.40        (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
   22.41        val maybe_spurious = Library.exists (fn
   22.42            Type (s, _) =>
   22.43 -          (case Datatype.get_datatype thy s of
   22.44 +          (case Datatype.get_info thy s of
   22.45              SOME info =>  (* inductive datatype *)
   22.46              let
   22.47                val index           = #index info
   22.48 @@ -1973,7 +1973,7 @@
   22.49      val (typs, terms) = model
   22.50      (* Term.typ -> (interpretation * model * arguments) option *)
   22.51      fun interpret_term (Type (s, Ts)) =
   22.52 -      (case Datatype.get_datatype thy s of
   22.53 +      (case Datatype.get_info thy s of
   22.54          SOME info =>  (* inductive datatype *)
   22.55          let
   22.56            (* int option -- only recursive IDTs have an associated depth *)
   22.57 @@ -2107,7 +2107,7 @@
   22.58              HOLogic_empty_set) pairss
   22.59          end
   22.60        | Type (s, Ts) =>
   22.61 -        (case Datatype.get_datatype thy s of
   22.62 +        (case Datatype.get_info thy s of
   22.63            SOME info =>
   22.64            (case AList.lookup (op =) typs T of
   22.65              SOME 0 =>
   22.66 @@ -2171,7 +2171,7 @@
   22.67          Const (s, T) =>
   22.68          (case body_type T of
   22.69            Type (s', Ts') =>
   22.70 -          (case Datatype.get_datatype thy s' of
   22.71 +          (case Datatype.get_info thy s' of
   22.72              SOME info =>  (* body type is an inductive datatype *)
   22.73              let
   22.74                val index               = #index info
   22.75 @@ -2652,7 +2652,7 @@
   22.76              end
   22.77            else
   22.78              NONE  (* not a recursion operator of this datatype *)
   22.79 -        ) (Datatype.get_datatypes thy) NONE
   22.80 +        ) (Datatype.get_all thy) NONE
   22.81      | _ =>  (* head of term is not a constant *)
   22.82        NONE;
   22.83  
   22.84 @@ -3201,7 +3201,7 @@
   22.85    fun IDT_printer thy model T intr assignment =
   22.86      (case T of
   22.87        Type (s, Ts) =>
   22.88 -      (case Datatype.get_datatype thy s of
   22.89 +      (case Datatype.get_info thy s of
   22.90          SOME info =>  (* inductive datatype *)
   22.91          let
   22.92            val (typs, _)           = model
    23.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Jun 23 21:05:51 2009 +0200
    23.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Jun 23 21:07:39 2009 +0200
    23.3 @@ -333,7 +333,7 @@
    23.4    let
    23.5      val cnstrs = flat (maps
    23.6        (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    23.7 -      (Symtab.dest (Datatype.get_datatypes thy)));
    23.8 +      (Symtab.dest (Datatype.get_all thy)));
    23.9      fun check t = (case strip_comb t of
   23.10          (Free _, []) => true
   23.11        | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
   23.12 @@ -875,7 +875,7 @@
   23.13  (* else false *)
   23.14  fun is_constructor thy t =
   23.15    if (is_Type (fastype_of t)) then
   23.16 -    (case Datatype.get_datatype thy ((fst o dest_Type o fastype_of) t) of
   23.17 +    (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
   23.18        NONE => false
   23.19      | SOME info => (let
   23.20        val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
   23.21 @@ -954,7 +954,7 @@
   23.22  fun prove_match thy (out_ts : term list) = let
   23.23    fun get_case_rewrite t =
   23.24      if (is_constructor thy t) then let
   23.25 -      val case_rewrites = (#case_rewrites (Datatype.the_datatype thy
   23.26 +      val case_rewrites = (#case_rewrites (Datatype.the_info thy
   23.27          ((fst o dest_Type o fastype_of) t)))
   23.28        in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
   23.29      else []
   23.30 @@ -1093,7 +1093,7 @@
   23.31    fun split_term_tac (Free _) = all_tac
   23.32      | split_term_tac t =
   23.33        if (is_constructor thy t) then let
   23.34 -        val info = Datatype.the_datatype thy ((fst o dest_Type o fastype_of) t)
   23.35 +        val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
   23.36          val num_of_constrs = length (#case_rewrites info)
   23.37          (* special treatment of pairs -- because of fishing *)
   23.38          val split_rules = case (fst o dest_Type o fastype_of) t of
    24.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Tue Jun 23 21:05:51 2009 +0200
    24.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Tue Jun 23 21:07:39 2009 +0200
    24.3 @@ -184,7 +184,7 @@
    24.4      val subgoal = Thm.term_of csubgoal;
    24.5    in
    24.6   (let
    24.7 -    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_datatypes) sign;
    24.8 +    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) sign;
    24.9      val concl = Logic.strip_imp_concl subgoal;
   24.10      val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
   24.11      val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));