do not open auxiliary ML structures;
authorwenzelm
Thu Dec 30 23:42:06 2010 +0100 (2010-12-30)
changeset 4142325df154b8ffc
parent 41422 8a765db7e0f8
child 41424 7ee22760436c
do not open auxiliary ML structures;
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/size.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Dec 30 22:34:53 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Dec 30 23:42:06 2010 +0100
     1.3 @@ -21,14 +21,11 @@
     1.4  
     1.5  (** auxiliary **)
     1.6  
     1.7 -open Datatype_Aux;
     1.8 -open Datatype_Data;
     1.9 -
    1.10  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    1.11  
    1.12  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    1.13  
    1.14 -fun exh_thm_of (dt_info : info Symtab.table) tname =
    1.15 +fun exh_thm_of (dt_info : Datatype_Aux.info Symtab.table) tname =
    1.16    #exhaust (the (Symtab.lookup dt_info tname));
    1.17  
    1.18  val node_name = @{type_name "Datatype.node"};
    1.19 @@ -60,7 +57,7 @@
    1.20  
    1.21  (** proof of characteristic theorems **)
    1.22  
    1.23 -fun representation_proofs (config : config) (dt_info : info Symtab.table)
    1.24 +fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table)
    1.25        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    1.26    let
    1.27      val descr' = flat descr;
    1.28 @@ -73,16 +70,16 @@
    1.29            (1 upto (length descr'))));
    1.30      val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
    1.31  
    1.32 -    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    1.33 -    val leafTs' = get_nonrec_types descr' sorts;
    1.34 -    val branchTs = get_branching_types descr' sorts;
    1.35 +    val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr);
    1.36 +    val leafTs' = Datatype_Aux.get_nonrec_types descr' sorts;
    1.37 +    val branchTs = Datatype_Aux.get_branching_types descr' sorts;
    1.38      val branchT = if null branchTs then HOLogic.unitT
    1.39        else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
    1.40 -    val arities = remove (op =) 0 (get_arities descr');
    1.41 +    val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
    1.42      val unneeded_vars =
    1.43        subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
    1.44      val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
    1.45 -    val recTs = get_rec_types descr' sorts;
    1.46 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    1.47      val (newTs, oldTs) = chop (length (hd descr)) recTs;
    1.48      val sumT = if null leafTs then HOLogic.unitT
    1.49        else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs;
    1.50 @@ -143,27 +140,27 @@
    1.51  
    1.52      (************** generate introduction rules for representing set **********)
    1.53  
    1.54 -    val _ = message config "Constructing representing sets ...";
    1.55 +    val _ = Datatype_Aux.message config "Constructing representing sets ...";
    1.56  
    1.57      (* make introduction rule for a single constructor *)
    1.58  
    1.59      fun make_intr s n (i, (_, cargs)) =
    1.60        let
    1.61          fun mk_prem dt (j, prems, ts) =
    1.62 -          (case strip_dtyp dt of
    1.63 -            (dts, DtRec k) =>
    1.64 +          (case Datatype_Aux.strip_dtyp dt of
    1.65 +            (dts, Datatype_Aux.DtRec k) =>
    1.66                let
    1.67 -                val Ts = map (typ_of_dtyp descr' sorts) dts;
    1.68 +                val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) dts;
    1.69                  val free_t =
    1.70 -                  app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
    1.71 +                  Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
    1.72                in (j + 1, list_all (map (pair "x") Ts,
    1.73                    HOLogic.mk_Trueprop
    1.74                      (Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
    1.75                  mk_lim free_t Ts :: ts)
    1.76                end
    1.77            | _ =>
    1.78 -              let val T = typ_of_dtyp descr' sorts dt
    1.79 -              in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
    1.80 +              let val T = Datatype_Aux.typ_of_dtyp descr' sorts dt
    1.81 +              in (j + 1, prems, (Leaf $ mk_inj T (Datatype_Aux.mk_Free "x" T j))::ts)
    1.82                end);
    1.83  
    1.84          val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
    1.85 @@ -221,17 +218,18 @@
    1.86      fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
    1.87        let
    1.88          fun constr_arg dt (j, l_args, r_args) =
    1.89 -          let val T = typ_of_dtyp descr' sorts dt;
    1.90 -              val free_t = mk_Free "x" T j
    1.91 -          in (case (strip_dtyp dt, strip_type T) of
    1.92 -              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
    1.93 +          let
    1.94 +            val T = Datatype_Aux.typ_of_dtyp descr' sorts dt;
    1.95 +            val free_t = Datatype_Aux.mk_Free "x" T j;
    1.96 +          in (case (Datatype_Aux.strip_dtyp dt, strip_type T) of
    1.97 +              ((_, Datatype_Aux.DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
    1.98                  (Const (nth all_rep_names m, U --> Univ_elT) $
    1.99 -                   app_bnds free_t (length Us)) Us :: r_args)
   1.100 +                   Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args)
   1.101              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   1.102            end;
   1.103  
   1.104          val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
   1.105 -        val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
   1.106 +        val constrT = (map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs) ---> T;
   1.107          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
   1.108          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
   1.109          val lhs = list_comb (Const (cname, constrT), l_args);
   1.110 @@ -276,7 +274,7 @@
   1.111  
   1.112      (*********** isomorphisms for new types (introduced by typedef) ***********)
   1.113  
   1.114 -    val _ = message config "Proving isomorphism properties ...";
   1.115 +    val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
   1.116  
   1.117      val newT_iso_axms = map (fn (_, (_, td)) =>
   1.118        (collect_simp (#Abs_inverse td), #Rep_inverse td,
   1.119 @@ -300,7 +298,7 @@
   1.120  
   1.121      fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
   1.122        let
   1.123 -        val argTs = map (typ_of_dtyp descr' sorts) cargs;
   1.124 +        val argTs = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   1.125          val T = nth recTs k;
   1.126          val rep_name = nth all_rep_names k;
   1.127          val rep_const = Const (rep_name, T --> Univ_elT);
   1.128 @@ -308,23 +306,23 @@
   1.129  
   1.130          fun process_arg ks' dt (i2, i2', ts, Ts) =
   1.131            let
   1.132 -            val T' = typ_of_dtyp descr' sorts dt;
   1.133 +            val T' = Datatype_Aux.typ_of_dtyp descr' sorts dt;
   1.134              val (Us, U) = strip_type T'
   1.135 -          in (case strip_dtyp dt of
   1.136 -              (_, DtRec j) => if member (op =) ks' j then
   1.137 -                  (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
   1.138 -                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
   1.139 +          in (case Datatype_Aux.strip_dtyp dt of
   1.140 +              (_, Datatype_Aux.DtRec j) => if member (op =) ks' j then
   1.141 +                  (i2 + 1, i2' + 1, ts @ [mk_lim (Datatype_Aux.app_bnds
   1.142 +                     (Datatype_Aux.mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
   1.143                     Ts @ [Us ---> Univ_elT])
   1.144                  else
   1.145                    (i2 + 1, i2', ts @ [mk_lim
   1.146                       (Const (nth all_rep_names j, U --> Univ_elT) $
   1.147 -                        app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
   1.148 -            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
   1.149 +                        Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" T' i2) (length Us)) Us], Ts)
   1.150 +            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (Datatype_Aux.mk_Free "x" T' i2)], Ts))
   1.151            end;
   1.152  
   1.153          val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []);
   1.154 -        val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
   1.155 -        val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
   1.156 +        val xs = map (uncurry (Datatype_Aux.mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
   1.157 +        val ys = map (uncurry (Datatype_Aux.mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
   1.158          val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
   1.159  
   1.160          val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []);
   1.161 @@ -383,9 +381,9 @@
   1.162              val f = Free ("f", Ts ---> U)
   1.163            in Skip_Proof.prove_global thy [] [] (Logic.mk_implies
   1.164              (HOLogic.mk_Trueprop (HOLogic.list_all
   1.165 -               (map (pair "x") Ts, S $ app_bnds f i)),
   1.166 +               (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
   1.167               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
   1.168 -               r $ (a $ app_bnds f i)), f))))
   1.169 +               r $ (a $ Datatype_Aux.app_bnds f i)), f))))
   1.170              (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
   1.171                 REPEAT (etac allE 1), rtac thm 1, atac 1])
   1.172            end
   1.173 @@ -407,9 +405,9 @@
   1.174              val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
   1.175              val rep_set_name = nth rep_set_names i
   1.176            in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
   1.177 -                HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
   1.178 -                  HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
   1.179 -              Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i))
   1.180 +                HOLogic.mk_eq (Rep_t $ Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $
   1.181 +                  HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)),
   1.182 +              Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i))
   1.183            end;
   1.184  
   1.185          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
   1.186 @@ -419,11 +417,11 @@
   1.187            map (fn r => r RS @{thm injD}) inj_thms;
   1.188  
   1.189          val inj_thm = Skip_Proof.prove_global thy5 [] []
   1.190 -          (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
   1.191 -            [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.192 +          (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1)) (fn _ => EVERY
   1.193 +            [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.194               REPEAT (EVERY
   1.195                 [rtac allI 1, rtac impI 1,
   1.196 -                exh_tac (exh_thm_of dt_info) 1,
   1.197 +                Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
   1.198                  REPEAT (EVERY
   1.199                    [hyp_subst_tac 1,
   1.200                     rewrite_goals_tac rewrites,
   1.201 @@ -440,17 +438,17 @@
   1.202                               Lim_inject :: inj_thms') @ fun_congs) 1),
   1.203                           atac 1]))])])])]);
   1.204  
   1.205 -        val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
   1.206 +        val inj_thms'' = map (fn r => r RS datatype_injI) (Datatype_Aux.split_conj_thm inj_thm);
   1.207  
   1.208          val elem_thm = 
   1.209 -            Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
   1.210 -              (fn _ =>
   1.211 -               EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.212 -                rewrite_goals_tac rewrites,
   1.213 -                REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
   1.214 -                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
   1.215 +          Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
   1.216 +            (fn _ =>
   1.217 +             EVERY [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.218 +              rewrite_goals_tac rewrites,
   1.219 +              REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
   1.220 +                ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
   1.221  
   1.222 -      in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
   1.223 +      in (inj_thms'' @ inj_thms, elem_thms @ (Datatype_Aux.split_conj_thm elem_thm))
   1.224        end;
   1.225  
   1.226      val (iso_inj_thms_unfolded, iso_elem_thms) =
   1.227 @@ -463,14 +461,14 @@
   1.228      fun mk_iso_t (((set_name, iso_name), i), T) =
   1.229        let val isoT = T --> Univ_elT
   1.230        in HOLogic.imp $ 
   1.231 -        (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
   1.232 +        (Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
   1.233            (if i < length newTs then HOLogic.true_const
   1.234 -           else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
   1.235 +           else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
   1.236               Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
   1.237                 Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
   1.238        end;
   1.239  
   1.240 -    val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
   1.241 +    val iso_t = HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (map mk_iso_t
   1.242        (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
   1.243  
   1.244      (* all the theorems are proved by one single simultaneous induction *)
   1.245 @@ -479,9 +477,9 @@
   1.246        iso_inj_thms_unfolded;
   1.247  
   1.248      val iso_thms = if length descr = 1 then [] else
   1.249 -      drop (length newTs) (split_conj_thm
   1.250 +      drop (length newTs) (Datatype_Aux.split_conj_thm
   1.251          (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
   1.252 -           [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.253 +           [(Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.254              REPEAT (rtac TrueI 1),
   1.255              rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
   1.256                Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
   1.257 @@ -502,7 +500,7 @@
   1.258  
   1.259      (******************* freeness theorems for constructors *******************)
   1.260  
   1.261 -    val _ = message config "Proving freeness of constructors ...";
   1.262 +    val _ = Datatype_Aux.message config "Proving freeness of constructors ...";
   1.263  
   1.264      (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
   1.265      
   1.266 @@ -566,12 +564,12 @@
   1.267      val ((constr_inject', distinct_thms'), thy6) =
   1.268        thy5
   1.269        |> Sign.parent_path
   1.270 -      |> store_thmss "inject" new_type_names constr_inject
   1.271 -      ||>> store_thmss "distinct" new_type_names distinct_thms;
   1.272 +      |> Datatype_Aux.store_thmss "inject" new_type_names constr_inject
   1.273 +      ||>> Datatype_Aux.store_thmss "distinct" new_type_names distinct_thms;
   1.274  
   1.275      (*************************** induction theorem ****************************)
   1.276  
   1.277 -    val _ = message config "Proving induction rule for datatypes ...";
   1.278 +    val _ = Datatype_Aux.message config "Proving induction rule for datatypes ...";
   1.279  
   1.280      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
   1.281        (map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded);
   1.282 @@ -580,7 +578,7 @@
   1.283      fun mk_indrule_lemma ((i, _), T) (prems, concls) =
   1.284        let
   1.285          val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $
   1.286 -          mk_Free "x" T i;
   1.287 +          Datatype_Aux.mk_Free "x" T i;
   1.288  
   1.289          val Abs_t = if i < length newTs then
   1.290              Const (Sign.intern_const thy6
   1.291 @@ -589,10 +587,13 @@
   1.292                [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
   1.293              HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
   1.294  
   1.295 -      in (prems @ [HOLogic.imp $
   1.296 +      in
   1.297 +        (prems @
   1.298 +          [HOLogic.imp $
   1.299              (Const (nth rep_set_names i, UnivT') $ Rep_t) $
   1.300 -              (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
   1.301 -          concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
   1.302 +              (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
   1.303 +         concls @
   1.304 +          [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i])
   1.305        end;
   1.306  
   1.307      val (indrule_lemma_prems, indrule_lemma_concls) =
   1.308 @@ -602,8 +603,8 @@
   1.309  
   1.310      val indrule_lemma = Skip_Proof.prove_global thy6 [] []
   1.311        (Logic.mk_implies
   1.312 -        (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   1.313 -         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   1.314 +        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
   1.315 +         HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY
   1.316             [REPEAT (etac conjE 1),
   1.317              REPEAT (EVERY
   1.318                [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
   1.319 @@ -619,7 +620,7 @@
   1.320        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.321        (fn {prems, ...} => EVERY
   1.322          [rtac indrule_lemma' 1,
   1.323 -         (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.324 +         (Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   1.325           EVERY (map (fn (prem, r) => (EVERY
   1.326             [REPEAT (eresolve_tac Abs_inverse_thms 1),
   1.327              simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
   1.328 @@ -680,7 +681,7 @@
   1.329                | vs => error ("Extra type variables on rhs: " ^ commas vs));
   1.330              val c = Sign.full_name_path tmp_thy tname' cname;
   1.331            in
   1.332 -            (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
   1.333 +            (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],
   1.334                constr_syntax' @ [(cname, mx')], sorts'')
   1.335            end handle ERROR msg => cat_error msg
   1.336             ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
   1.337 @@ -691,7 +692,7 @@
   1.338        in
   1.339          case duplicates (op =) (map fst constrs') of
   1.340            [] =>
   1.341 -            (dts' @ [(i, (Sign.full_name tmp_thy tname, map DtTFree tvs, constrs'))],
   1.342 +            (dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
   1.343                constr_syntax @ [constr_syntax'], sorts', i + 1)
   1.344          | dups => error ("Duplicate constructors " ^ commas dups ^
   1.345               " in datatype " ^ quote (Binding.str_of tname))
   1.346 @@ -701,12 +702,14 @@
   1.347        fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
   1.348      val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
   1.349      val dt_info = Datatype_Data.get_all thy;
   1.350 -    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   1.351 -    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   1.352 -      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   1.353 -      else reraise exn;
   1.354 +    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   1.355 +    val _ =
   1.356 +      Datatype_Aux.check_nonempty descr
   1.357 +        handle (exn as Datatype_Aux.Datatype_Empty s) =>
   1.358 +          if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   1.359 +          else reraise exn;
   1.360  
   1.361 -    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   1.362 +    val _ = Datatype_Aux.message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   1.363  
   1.364    in
   1.365      thy
   1.366 @@ -718,7 +721,7 @@
   1.367    end;
   1.368  
   1.369  val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
   1.370 -val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ default_config;
   1.371 +val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config;
   1.372  
   1.373  local
   1.374  
   1.375 @@ -745,4 +748,7 @@
   1.376  
   1.377  end;
   1.378  
   1.379 +
   1.380 +open Datatype_Data;
   1.381 +
   1.382  end;
     2.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Dec 30 22:34:53 2010 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Dec 30 23:42:06 2010 +0100
     2.3 @@ -35,16 +35,15 @@
     2.4  structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
     2.5  struct
     2.6  
     2.7 -open Datatype_Aux;
     2.8 -
     2.9  (************************ case distinction theorems ***************************)
    2.10  
    2.11 -fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
    2.12 +fun prove_casedist_thms (config : Datatype_Aux.config)
    2.13 +    new_type_names descr sorts induct case_names_exhausts thy =
    2.14    let
    2.15 -    val _ = message config "Proving case distinction theorems ...";
    2.16 +    val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
    2.17  
    2.18      val descr' = flat descr;
    2.19 -    val recTs = get_rec_types descr' sorts;
    2.20 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    2.21      val newTs = take (length (hd descr)) recTs;
    2.22  
    2.23      val {maxidx, ...} = rep_thm induct;
    2.24 @@ -60,7 +59,7 @@
    2.25          val cert = cterm_of thy;
    2.26          val insts' = (map cert induct_Ps) ~~ (map cert insts);
    2.27          val induct' = refl RS ((nth
    2.28 -          (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
    2.29 +          (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
    2.30  
    2.31        in
    2.32          Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    2.33 @@ -75,22 +74,23 @@
    2.34        (newTs ~~ Datatype_Prop.make_casedists descr sorts)
    2.35    in
    2.36      thy
    2.37 -    |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
    2.38 +    |> Datatype_Aux.store_thms_atts "exhaust" new_type_names
    2.39 +      (map single case_names_exhausts) casedist_thms
    2.40    end;
    2.41  
    2.42  
    2.43  (*************************** primrec combinators ******************************)
    2.44  
    2.45 -fun prove_primrec_thms (config : config) new_type_names descr sorts
    2.46 +fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr sorts
    2.47      injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
    2.48    let
    2.49 -    val _ = message config "Constructing primrec combinators ...";
    2.50 +    val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
    2.51  
    2.52      val big_name = space_implode "_" new_type_names;
    2.53      val thy0 = Sign.add_path big_name thy;
    2.54  
    2.55      val descr' = flat descr;
    2.56 -    val recTs = get_rec_types descr' sorts;
    2.57 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    2.58      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    2.59      val newTs = take (length (hd descr)) recTs;
    2.60  
    2.61 @@ -108,7 +108,7 @@
    2.62      val rec_set_Ts = map (fn (T1, T2) =>
    2.63        reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
    2.64  
    2.65 -    val rec_fns = map (uncurry (mk_Free "f"))
    2.66 +    val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
    2.67        (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
    2.68      val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
    2.69        (rec_set_names' ~~ rec_set_Ts);
    2.70 @@ -120,21 +120,21 @@
    2.71      fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
    2.72        let
    2.73          fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
    2.74 -          let val free1 = mk_Free "x" U j
    2.75 -          in (case (strip_dtyp dt, strip_type U) of
    2.76 -             ((_, DtRec m), (Us, _)) =>
    2.77 +          let val free1 = Datatype_Aux.mk_Free "x" U j
    2.78 +          in (case (Datatype_Aux.strip_dtyp dt, strip_type U) of
    2.79 +             ((_, Datatype_Aux.DtRec m), (Us, _)) =>
    2.80                 let
    2.81 -                 val free2 = mk_Free "y" (Us ---> nth rec_result_Ts m) k;
    2.82 +                 val free2 = Datatype_Aux.mk_Free "y" (Us ---> nth rec_result_Ts m) k;
    2.83                   val i = length Us
    2.84                 in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
    2.85                       (map (pair "x") Us, nth rec_sets' m $
    2.86 -                       app_bnds free1 i $ app_bnds free2 i)) :: prems,
    2.87 +                       Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
    2.88                     free1::t1s, free2::t2s)
    2.89                 end
    2.90             | _ => (j + 1, k, prems, free1::t1s, t2s))
    2.91            end;
    2.92  
    2.93 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
    2.94 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
    2.95          val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
    2.96  
    2.97        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
    2.98 @@ -160,7 +160,7 @@
    2.99  
   2.100      (* prove uniqueness and termination of primrec combinators *)
   2.101  
   2.102 -    val _ = message config "Proving termination and uniqueness of primrec functions ...";
   2.103 +    val _ = Datatype_Aux.message config "Proving termination and uniqueness of primrec functions ...";
   2.104  
   2.105      fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
   2.106        let
   2.107 @@ -175,7 +175,7 @@
   2.108  
   2.109          fun mk_unique_constr_tac n (cname, cargs) (tac, intr::intrs, j) =
   2.110            let
   2.111 -            val k = length (filter is_rec_type cargs)
   2.112 +            val k = length (filter Datatype_Aux.is_rec_type cargs)
   2.113  
   2.114            in (EVERY [DETERM tac,
   2.115                  REPEAT (etac ex1E 1), rtac ex1I 1,
   2.116 @@ -201,7 +201,7 @@
   2.117        let
   2.118          val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
   2.119            Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
   2.120 -            absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
   2.121 +            absfree ("y", T2, set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
   2.122                (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
   2.123          val cert = cterm_of thy1
   2.124          val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
   2.125 @@ -212,8 +212,9 @@
   2.126             (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
   2.127                THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
   2.128  
   2.129 -      in split_conj_thm (Skip_Proof.prove_global thy1 [] []
   2.130 -        (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
   2.131 +      in
   2.132 +        Datatype_Aux.split_conj_thm (Skip_Proof.prove_global thy1 [] []
   2.133 +          (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts)) (K tac))
   2.134        end;
   2.135  
   2.136      val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
   2.137 @@ -247,7 +248,7 @@
   2.138  
   2.139      (* prove characteristic equations for primrec combinators *)
   2.140  
   2.141 -    val _ = message config "Proving characteristic theorems for primrec combinators ..."
   2.142 +    val _ = Datatype_Aux.message config "Proving characteristic theorems for primrec combinators ...";
   2.143  
   2.144      val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
   2.145        (fn _ => EVERY
   2.146 @@ -256,8 +257,7 @@
   2.147           resolve_tac rec_unique_thms 1,
   2.148           resolve_tac rec_intrs 1,
   2.149           REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   2.150 -           (Datatype_Prop.make_primrecs new_type_names descr sorts thy2)
   2.151 -
   2.152 +           (Datatype_Prop.make_primrecs new_type_names descr sorts thy2);
   2.153    in
   2.154      thy2
   2.155      |> Sign.add_path (space_implode "_" new_type_names)
   2.156 @@ -270,24 +270,25 @@
   2.157  
   2.158  (***************************** case combinators *******************************)
   2.159  
   2.160 -fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
   2.161 +fun prove_case_thms (config : Datatype_Aux.config)
   2.162 +    new_type_names descr sorts reccomb_names primrec_thms thy =
   2.163    let
   2.164 -    val _ = message config "Proving characteristic theorems for case combinators ...";
   2.165 +    val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
   2.166  
   2.167      val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
   2.168  
   2.169      val descr' = flat descr;
   2.170 -    val recTs = get_rec_types descr' sorts;
   2.171 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   2.172      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   2.173      val newTs = take (length (hd descr)) recTs;
   2.174      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   2.175  
   2.176 -    fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
   2.177 +    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
   2.178  
   2.179      val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   2.180        let
   2.181 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   2.182 -        val Ts' = map mk_dummyT (filter is_rec_type cargs)
   2.183 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   2.184 +        val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
   2.185        in Const (@{const_name undefined}, Ts @ Ts' ---> T')
   2.186        end) constrs) descr';
   2.187  
   2.188 @@ -299,11 +300,11 @@
   2.189          let
   2.190            val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
   2.191              let
   2.192 -              val Ts = map (typ_of_dtyp descr' sorts) cargs;
   2.193 -              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
   2.194 -              val frees' = map2 (mk_Free "x") Ts' (1 upto length Ts');
   2.195 +              val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   2.196 +              val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
   2.197 +              val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
   2.198                val frees = take (length cargs) frees';
   2.199 -              val free = mk_Free "f" (Ts ---> T') j
   2.200 +              val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j
   2.201              in
   2.202               (free, list_abs_free (map dest_Free frees',
   2.203                 list_comb (free, frees)))
   2.204 @@ -335,20 +336,20 @@
   2.205      thy2
   2.206      |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
   2.207      |> Sign.parent_path
   2.208 -    |> store_thmss "cases" new_type_names case_thms
   2.209 +    |> Datatype_Aux.store_thmss "cases" new_type_names case_thms
   2.210      |-> (fn thmss => pair (thmss, case_names))
   2.211    end;
   2.212  
   2.213  
   2.214  (******************************* case splitting *******************************)
   2.215  
   2.216 -fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
   2.217 -    casedist_thms case_thms thy =
   2.218 +fun prove_split_thms (config : Datatype_Aux.config)
   2.219 +    new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy =
   2.220    let
   2.221 -    val _ = message config "Proving equations for case splitting ...";
   2.222 +    val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
   2.223  
   2.224      val descr' = flat descr;
   2.225 -    val recTs = get_rec_types descr' sorts;
   2.226 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   2.227      val newTs = take (length (hd descr)) recTs;
   2.228  
   2.229      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
   2.230 @@ -373,8 +374,8 @@
   2.231  
   2.232    in
   2.233      thy
   2.234 -    |> store_thms "split" new_type_names split_thms
   2.235 -    ||>> store_thms "split_asm" new_type_names split_asm_thms
   2.236 +    |> Datatype_Aux.store_thms "split" new_type_names split_thms
   2.237 +    ||>> Datatype_Aux.store_thms "split_asm" new_type_names split_asm_thms
   2.238      |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   2.239    end;
   2.240  
   2.241 @@ -387,13 +388,14 @@
   2.242      val weak_case_congs = map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs
   2.243        new_type_names descr sorts thy)
   2.244  
   2.245 -  in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end;
   2.246 +  in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
   2.247  
   2.248  (************************* additional theorems for TFL ************************)
   2.249  
   2.250 -fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
   2.251 +fun prove_nchotomys (config : Datatype_Aux.config)
   2.252 +    new_type_names descr sorts casedist_thms thy =
   2.253    let
   2.254 -    val _ = message config "Proving additional theorems for TFL ...";
   2.255 +    val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
   2.256  
   2.257      fun prove_nchotomy (t, exhaustion) =
   2.258        let
   2.259 @@ -404,14 +406,14 @@
   2.260        in 
   2.261          Skip_Proof.prove_global thy [] [] t (fn _ =>
   2.262            EVERY [rtac allI 1,
   2.263 -           exh_tac (K exhaustion) 1,
   2.264 +           Datatype_Aux.exh_tac (K exhaustion) 1,
   2.265             ALLGOALS (fn i => tac i (i-1))])
   2.266        end;
   2.267  
   2.268      val nchotomys =
   2.269        map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms)
   2.270  
   2.271 -  in thy |> store_thms "nchotomy" new_type_names nchotomys end;
   2.272 +  in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
   2.273  
   2.274  fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
   2.275    let
   2.276 @@ -437,6 +439,9 @@
   2.277      val case_congs = map prove_case_cong (Datatype_Prop.make_case_congs
   2.278        new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
   2.279  
   2.280 -  in thy |> store_thms "case_cong" new_type_names case_congs end;
   2.281 +  in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
   2.282 +
   2.283 +
   2.284 +open Datatype_Aux;
   2.285  
   2.286  end;
     3.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 30 22:34:53 2010 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 30 23:42:06 2010 +0100
     3.3 @@ -37,8 +37,6 @@
     3.4  structure Datatype_Data: DATATYPE_DATA =
     3.5  struct
     3.6  
     3.7 -open Datatype_Aux;
     3.8 -
     3.9  (** theory data **)
    3.10  
    3.11  (* data management *)
    3.12 @@ -46,9 +44,9 @@
    3.13  structure DatatypesData = Theory_Data
    3.14  (
    3.15    type T =
    3.16 -    {types: info Symtab.table,
    3.17 -     constrs: (string * info) list Symtab.table,
    3.18 -     cases: info Symtab.table};
    3.19 +    {types: Datatype_Aux.info Symtab.table,
    3.20 +     constrs: (string * Datatype_Aux.info) list Symtab.table,
    3.21 +     cases: Datatype_Aux.info Symtab.table};
    3.22  
    3.23    val empty =
    3.24      {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
    3.25 @@ -85,7 +83,7 @@
    3.26  
    3.27  val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
    3.28  
    3.29 -fun register (dt_infos : (string * info) list) =
    3.30 +fun register (dt_infos : (string * Datatype_Aux.info) list) =
    3.31    DatatypesData.map (fn {types, constrs, cases} =>
    3.32      {types = types |> fold Symtab.update dt_infos,
    3.33       constrs = constrs |> fold (fn (constr, dtname_info) =>
    3.34 @@ -116,13 +114,15 @@
    3.35  
    3.36      val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
    3.37      val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
    3.38 -      o dest_DtTFree) dtys;
    3.39 +      o Datatype_Aux.dest_DtTFree) dtys;
    3.40  
    3.41 -    fun is_DtTFree (DtTFree _) = true
    3.42 +    fun is_DtTFree (Datatype_Aux.DtTFree _) = true
    3.43        | is_DtTFree _ = false
    3.44      val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
    3.45 -    val protoTs as (dataTs, _) = chop k descr
    3.46 -      |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
    3.47 +    val protoTs as (dataTs, _) =
    3.48 +      chop k descr
    3.49 +      |> (pairself o map)
    3.50 +        (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
    3.51      
    3.52      val tycos = map fst dataTs;
    3.53      val _ = if eq_set (op =) (tycos, raw_tycos) then ()
    3.54 @@ -133,7 +133,7 @@
    3.55  
    3.56      val names = map Long_Name.base_name (the_default tycos (#alt_names info));
    3.57      val (auxnames, _) = Name.make_context names
    3.58 -      |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
    3.59 +      |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us;
    3.60      val prefix = space_implode "_" names;
    3.61  
    3.62    in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
    3.63 @@ -186,11 +186,11 @@
    3.64  
    3.65  local
    3.66  
    3.67 -fun dt_recs (DtTFree _) = []
    3.68 -  | dt_recs (DtType (_, dts)) = maps dt_recs dts
    3.69 -  | dt_recs (DtRec i) = [i];
    3.70 +fun dt_recs (Datatype_Aux.DtTFree _) = []
    3.71 +  | dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts
    3.72 +  | dt_recs (Datatype_Aux.DtRec i) = [i];
    3.73  
    3.74 -fun dt_cases (descr: descr) (_, args, constrs) =
    3.75 +fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) =
    3.76    let
    3.77      fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
    3.78      val bnames = map the_bname (distinct (op =) (maps dt_recs args));
    3.79 @@ -264,7 +264,7 @@
    3.80  (** abstract theory extensions relative to a datatype characterisation **)
    3.81  
    3.82  structure Datatype_Interpretation = Interpretation
    3.83 -  (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    3.84 +  (type T = Datatype_Aux.config * string list val eq: T * T -> bool = eq_snd op =);
    3.85  fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
    3.86  
    3.87  fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
    3.88 @@ -297,7 +297,9 @@
    3.89      val thy2 = thy1 |> Theory.checkpoint;
    3.90      val flat_descr = flat descr;
    3.91      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    3.92 -    val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
    3.93 +    val _ =
    3.94 +      Datatype_Aux.message config
    3.95 +        ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
    3.96  
    3.97      val (exhaust, thy3) = Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
    3.98        descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
    3.99 @@ -305,7 +307,7 @@
   3.100        descr sorts exhaust thy3;
   3.101      val ((rec_names, rec_rewrites), thy5) = Datatype_Abs_Proofs.prove_primrec_thms
   3.102        config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
   3.103 -      inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts))
   3.104 +      inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr sorts))
   3.105        induct thy4;
   3.106      val ((case_rewrites, case_names), thy6) = Datatype_Abs_Proofs.prove_case_thms
   3.107        config new_type_names descr sorts rec_names rec_rewrites thy5;
   3.108 @@ -363,8 +365,8 @@
   3.109      val prfx = Binding.qualify true (space_implode "_" new_type_names);
   3.110      val (((inject, distinct), [induct]), thy2) =
   3.111        thy1
   3.112 -      |> store_thmss "inject" new_type_names raw_inject
   3.113 -      ||>> store_thmss "distinct" new_type_names raw_distinct
   3.114 +      |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject
   3.115 +      ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct
   3.116        ||>> Global_Theory.add_thms
   3.117          [((prfx (Binding.name "induct"), raw_induct),
   3.118            [mk_case_names_induct descr])];
   3.119 @@ -411,11 +413,11 @@
   3.120  
   3.121      val cs = map (apsnd (map norm_constr)) raw_cs;
   3.122      val dtyps_of_typ =
   3.123 -      map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
   3.124 +      map (Datatype_Aux.dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
   3.125      val dt_names = map fst cs;
   3.126  
   3.127      fun mk_spec (i, (tyco, constr)) = (i, (tyco,
   3.128 -      map (DtTFree o fst) vs,
   3.129 +      map (Datatype_Aux.DtTFree o fst) vs,
   3.130        (map o apsnd) dtyps_of_typ constr))
   3.131      val descr = map_index mk_spec cs;
   3.132      val injs = Datatype_Prop.make_injs [descr] vs;
   3.133 @@ -441,7 +443,7 @@
   3.134    end;
   3.135  
   3.136  val rep_datatype = gen_rep_datatype Sign.cert_term;
   3.137 -val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
   3.138 +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global Datatype_Aux.default_config (K I);
   3.139  
   3.140  
   3.141  
   3.142 @@ -463,4 +465,7 @@
   3.143        >> (fn (alt_names, ts) =>
   3.144          Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
   3.145  
   3.146 +
   3.147 +open Datatype_Aux;
   3.148 +
   3.149  end;
     4.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Dec 30 22:34:53 2010 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Dec 30 23:42:06 2010 +0100
     4.3 @@ -35,8 +35,6 @@
     4.4  structure Datatype_Prop : DATATYPE_PROP =
     4.5  struct
     4.6  
     4.7 -open Datatype_Aux;
     4.8 -
     4.9  fun indexify_names names =
    4.10    let
    4.11      fun index (x :: xs) tab =
    4.12 @@ -63,7 +61,7 @@
    4.13      fun make_inj T (cname, cargs) =
    4.14        if null cargs then I else
    4.15          let
    4.16 -          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.17 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
    4.18            val constr_t = Const (cname, Ts ---> T);
    4.19            val tnames = make_tnames Ts;
    4.20            val frees = map Free (tnames ~~ Ts);
    4.21 @@ -75,7 +73,7 @@
    4.22          end;
    4.23    in
    4.24      map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
    4.25 -      (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts))
    4.26 +      (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
    4.27    end;
    4.28  
    4.29  
    4.30 @@ -84,10 +82,10 @@
    4.31  fun make_distincts descr sorts =
    4.32    let
    4.33      val descr' = flat descr;
    4.34 -    val recTs = get_rec_types descr' sorts;
    4.35 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    4.36      val newTs = take (length (hd descr)) recTs;
    4.37  
    4.38 -    fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
    4.39 +    fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
    4.40  
    4.41      fun make_distincts' _ [] = []
    4.42        | make_distincts' T ((cname, cargs)::constrs) =
    4.43 @@ -117,8 +115,9 @@
    4.44  fun make_ind descr sorts =
    4.45    let
    4.46      val descr' = flat descr;
    4.47 -    val recTs = get_rec_types descr' sorts;
    4.48 -    val pnames = if length descr' = 1 then ["P"]
    4.49 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    4.50 +    val pnames =
    4.51 +      if length descr' = 1 then ["P"]
    4.52        else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
    4.53  
    4.54      fun make_pred i T =
    4.55 @@ -129,15 +128,18 @@
    4.56        let
    4.57          fun mk_prem ((dt, s), T) =
    4.58            let val (Us, U) = strip_type T
    4.59 -          in list_all (map (pair "x") Us, HOLogic.mk_Trueprop
    4.60 -            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
    4.61 +          in
    4.62 +            list_all (map (pair "x") Us,
    4.63 +              HOLogic.mk_Trueprop
    4.64 +                (make_pred (Datatype_Aux.body_index dt) U $
    4.65 +                  Datatype_Aux.app_bnds (Free (s, T)) (length Us)))
    4.66            end;
    4.67  
    4.68 -        val recs = filter is_rec_type cargs;
    4.69 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.70 -        val recTs' = map (typ_of_dtyp descr' sorts) recs;
    4.71 +        val recs = filter Datatype_Aux.is_rec_type cargs;
    4.72 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
    4.73 +        val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
    4.74          val tnames = Name.variant_list pnames (make_tnames Ts);
    4.75 -        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
    4.76 +        val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
    4.77          val frees = tnames ~~ Ts;
    4.78          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
    4.79  
    4.80 @@ -163,7 +165,7 @@
    4.81  
    4.82      fun make_casedist_prem T (cname, cargs) =
    4.83        let
    4.84 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.85 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
    4.86          val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
    4.87          val free_ts = map Free frees
    4.88        in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
    4.89 @@ -176,7 +178,10 @@
    4.90        in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
    4.91        end
    4.92  
    4.93 -  in map2 make_casedist (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts)) end;
    4.94 +  in
    4.95 +    map2 make_casedist (hd descr)
    4.96 +      (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
    4.97 +  end;
    4.98  
    4.99  (*************** characteristic equations for primrec combinator **************)
   4.100  
   4.101 @@ -190,11 +195,11 @@
   4.102      val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
   4.103        map (fn (_, cargs) =>
   4.104          let
   4.105 -          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   4.106 -          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
   4.107 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   4.108 +          val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
   4.109  
   4.110            fun mk_argT (dt, T) =
   4.111 -            binder_types T ---> List.nth (rec_result_Ts, body_index dt);
   4.112 +            binder_types T ---> List.nth (rec_result_Ts, Datatype_Aux.body_index dt);
   4.113  
   4.114            val argTs = Ts @ map mk_argT recs
   4.115          in argTs ---> List.nth (rec_result_Ts, i)
   4.116 @@ -205,12 +210,12 @@
   4.117  fun make_primrecs new_type_names descr sorts thy =
   4.118    let
   4.119      val descr' = flat descr;
   4.120 -    val recTs = get_rec_types descr' sorts;
   4.121 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   4.122      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   4.123  
   4.124      val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   4.125  
   4.126 -    val rec_fns = map (uncurry (mk_Free "f"))
   4.127 +    val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
   4.128        (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
   4.129  
   4.130      val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   4.131 @@ -224,18 +229,18 @@
   4.132  
   4.133      fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =
   4.134        let
   4.135 -        val recs = filter is_rec_type cargs;
   4.136 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   4.137 -        val recTs' = map (typ_of_dtyp descr' sorts) recs;
   4.138 +        val recs = filter Datatype_Aux.is_rec_type cargs;
   4.139 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   4.140 +        val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
   4.141          val tnames = make_tnames Ts;
   4.142 -        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   4.143 +        val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
   4.144          val frees = map Free (tnames ~~ Ts);
   4.145          val frees' = map Free (rec_tnames ~~ recTs');
   4.146  
   4.147          fun mk_reccomb ((dt, T), t) =
   4.148            let val (Us, U) = strip_type T
   4.149            in list_abs (map (pair "x") Us,
   4.150 -            List.nth (reccombs, body_index dt) $ app_bnds t (length Us))
   4.151 +            List.nth (reccombs, Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
   4.152            end;
   4.153  
   4.154          val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
   4.155 @@ -256,14 +261,14 @@
   4.156  fun make_case_combs new_type_names descr sorts thy fname =
   4.157    let
   4.158      val descr' = flat descr;
   4.159 -    val recTs = get_rec_types descr' sorts;
   4.160 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   4.161      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   4.162      val newTs = take (length (hd descr)) recTs;
   4.163      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   4.164  
   4.165      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   4.166        map (fn (_, cargs) =>
   4.167 -        let val Ts = map (typ_of_dtyp descr' sorts) cargs
   4.168 +        let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs
   4.169          in Ts ---> T' end) constrs) (hd descr);
   4.170  
   4.171      val case_names = map (fn s =>
   4.172 @@ -271,7 +276,7 @@
   4.173    in
   4.174      map (fn ((name, Ts), T) => list_comb
   4.175        (Const (name, Ts @ [T] ---> T'),
   4.176 -        map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
   4.177 +        map (uncurry (Datatype_Aux.mk_Free fname)) (Ts ~~ (1 upto length Ts))))
   4.178            (case_names ~~ case_fn_Ts ~~ newTs)
   4.179    end;
   4.180  
   4.181 @@ -280,12 +285,12 @@
   4.182  fun make_cases new_type_names descr sorts thy =
   4.183    let
   4.184      val descr' = flat descr;
   4.185 -    val recTs = get_rec_types descr' sorts;
   4.186 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   4.187      val newTs = take (length (hd descr)) recTs;
   4.188  
   4.189      fun make_case T comb_t ((cname, cargs), f) =
   4.190        let
   4.191 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   4.192 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   4.193          val frees = map Free ((make_tnames Ts) ~~ Ts)
   4.194        in HOLogic.mk_Trueprop (HOLogic.mk_eq
   4.195          (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
   4.196 @@ -303,7 +308,7 @@
   4.197  fun make_splits new_type_names descr sorts thy =
   4.198    let
   4.199      val descr' = flat descr;
   4.200 -    val recTs = get_rec_types descr' sorts;
   4.201 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   4.202      val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   4.203      val newTs = take (length (hd descr)) recTs;
   4.204      val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   4.205 @@ -316,7 +321,7 @@
   4.206  
   4.207          fun process_constr ((cname, cargs), f) (t1s, t2s) =
   4.208            let
   4.209 -            val Ts = map (typ_of_dtyp descr' sorts) cargs;
   4.210 +            val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   4.211              val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
   4.212              val eqn = HOLogic.mk_eq (Free ("x", T),
   4.213                list_comb (Const (cname, Ts ---> T), frees));
   4.214 @@ -330,8 +335,8 @@
   4.215          val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
   4.216          val lhs = P $ (comb_t $ Free ("x", T))
   4.217        in
   4.218 -        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
   4.219 -         HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ mk_disj t2s)))
   4.220 +        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Datatype_Aux.mk_conj t1s)),
   4.221 +         HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Datatype_Aux.mk_disj t2s)))
   4.222        end
   4.223  
   4.224    in map make_split ((hd descr) ~~ newTs ~~
   4.225 @@ -415,12 +420,12 @@
   4.226  fun make_nchotomys descr sorts =
   4.227    let
   4.228      val descr' = flat descr;
   4.229 -    val recTs = get_rec_types descr' sorts;
   4.230 +    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   4.231      val newTs = take (length (hd descr)) recTs;
   4.232  
   4.233      fun mk_eqn T (cname, cargs) =
   4.234        let
   4.235 -        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   4.236 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   4.237          val tnames = Name.variant_list ["v"] (make_tnames Ts);
   4.238          val frees = tnames ~~ Ts
   4.239        in
   4.240 @@ -430,8 +435,11 @@
   4.241        end
   4.242  
   4.243    in map (fn ((_, (_, _, constrs)), T) =>
   4.244 -    HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, mk_disj (map (mk_eqn T) constrs))))
   4.245 +    HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
   4.246        (hd descr ~~ newTs)
   4.247    end;
   4.248  
   4.249 +
   4.250 +open Datatype_Aux;
   4.251 +
   4.252  end;
     5.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Dec 30 22:34:53 2010 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Dec 30 23:42:06 2010 +0100
     5.3 @@ -14,8 +14,6 @@
     5.4  structure Datatype_Realizer : DATATYPE_REALIZER =
     5.5  struct
     5.6  
     5.7 -open Datatype_Aux;
     5.8 -
     5.9  fun subsets i j =
    5.10    if i <= j then
    5.11      let val is = subsets (i+1) j
    5.12 @@ -30,9 +28,9 @@
    5.13  fun tname_of (Type (s, _)) = s
    5.14    | tname_of _ = "";
    5.15  
    5.16 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
    5.17 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
    5.18    let
    5.19 -    val recTs = get_rec_types descr sorts;
    5.20 +    val recTs = Datatype_Aux.get_rec_types descr sorts;
    5.21      val pnames = if length descr = 1 then ["P"]
    5.22        else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
    5.23  
    5.24 @@ -51,16 +49,16 @@
    5.25      val (prems, rec_fns) = split_list (flat (fst (fold_map
    5.26        (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    5.27          let
    5.28 -          val Ts = map (typ_of_dtyp descr sorts) cargs;
    5.29 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
    5.30            val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
    5.31 -          val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    5.32 +          val recs = filter (Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    5.33            val frees = tnames ~~ Ts;
    5.34  
    5.35            fun mk_prems vs [] =
    5.36                  let
    5.37                    val rT = nth (rec_result_Ts) i;
    5.38                    val vs' = filter_out is_unit vs;
    5.39 -                  val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
    5.40 +                  val f = Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
    5.41                    val f' = Envir.eta_contract (list_abs_free
    5.42                      (map dest_Free vs, if member (op =) is i then list_comb (f, vs')
    5.43                        else HOLogic.unit));
    5.44 @@ -69,7 +67,7 @@
    5.45                  end
    5.46              | mk_prems vs (((dt, s), T) :: ds) =
    5.47                  let
    5.48 -                  val k = body_index dt;
    5.49 +                  val k = Datatype_Aux.body_index dt;
    5.50                    val (Us, U) = strip_type T;
    5.51                    val i = length Us;
    5.52                    val rT = nth (rec_result_Ts) k;
    5.53 @@ -77,8 +75,8 @@
    5.54                    val (p, f) = mk_prems (vs @ [r]) ds
    5.55                  in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    5.56                    (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
    5.57 -                    (make_pred k rT U (app_bnds r i)
    5.58 -                      (app_bnds (Free (s, T)) i))), p)), f)
    5.59 +                    (make_pred k rT U (Datatype_Aux.app_bnds r i)
    5.60 +                      (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
    5.61                  end
    5.62  
    5.63          in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
    5.64 @@ -154,7 +152,8 @@
    5.65    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    5.66  
    5.67  
    5.68 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaust, ...} : info) thy =
    5.69 +fun make_casedists sorts
    5.70 +    ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
    5.71    let
    5.72      val cert = cterm_of thy;
    5.73      val rT = TFree ("'P", HOLogic.typeS);
    5.74 @@ -162,7 +161,7 @@
    5.75  
    5.76      fun make_casedist_prem T (cname, cargs) =
    5.77        let
    5.78 -        val Ts = map (typ_of_dtyp descr sorts) cargs;
    5.79 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
    5.80          val frees = Name.variant_list ["P", "y"] (Datatype_Prop.make_tnames Ts) ~~ Ts;
    5.81          val free_ts = map Free frees;
    5.82          val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
    5.83 @@ -173,7 +172,7 @@
    5.84        end;
    5.85  
    5.86      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
    5.87 -    val T = List.nth (get_rec_types descr sorts, index);
    5.88 +    val T = List.nth (Datatype_Aux.get_rec_types descr sorts, index);
    5.89      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
    5.90      val r = Const (case_name, map fastype_of rs ---> T --> rT);
    5.91  
    5.92 @@ -218,7 +217,7 @@
    5.93    if ! Proofterm.proofs < 2 then thy
    5.94    else
    5.95      let
    5.96 -      val _ = message config "Adding realizers for induction and case analysis ..."
    5.97 +      val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
    5.98        val infos = map (Datatype.the_info thy) names;
    5.99        val info :: _ = infos;
   5.100      in
     6.1 --- a/src/HOL/Tools/Function/size.ML	Thu Dec 30 22:34:53 2010 +0100
     6.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Dec 30 23:42:06 2010 +0100
     6.3 @@ -42,7 +42,7 @@
     6.4        NONE => Abs ("x", T, HOLogic.zero)
     6.5      | SOME t => t);
     6.6  
     6.7 -fun is_poly thy (DtType (name, dts)) =
     6.8 +fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
     6.9        (case Datatype.get_info thy name of
    6.10           NONE => false
    6.11         | SOME _ => exists (is_poly thy) dts)