# HG changeset patch
# User wenzelm
# Date 1293748926 -3600
# Node ID 25df154b8ffce4bde37a170140b9d3796f3fb115
# Parent  8a765db7e0f89190d528071d79cddccea0bb5fc3
do not open auxiliary ML structures;

diff -r 8a765db7e0f8 -r 25df154b8ffc src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Dec 30 23:42:06 2010 +0100
@@ -21,14 +21,11 @@
 
 (** auxiliary **)
 
-open Datatype_Aux;
-open Datatype_Data;
-
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
 
 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
 
-fun exh_thm_of (dt_info : info Symtab.table) tname =
+fun exh_thm_of (dt_info : Datatype_Aux.info Symtab.table) tname =
   #exhaust (the (Symtab.lookup dt_info tname));
 
 val node_name = @{type_name "Datatype.node"};
@@ -60,7 +57,7 @@
 
 (** proof of characteristic theorems **)
 
-fun representation_proofs (config : config) (dt_info : info Symtab.table)
+fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
     val descr' = flat descr;
@@ -73,16 +70,16 @@
           (1 upto (length descr'))));
     val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
 
-    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
-    val leafTs' = get_nonrec_types descr' sorts;
-    val branchTs = get_branching_types descr' sorts;
+    val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr);
+    val leafTs' = Datatype_Aux.get_nonrec_types descr' sorts;
+    val branchTs = Datatype_Aux.get_branching_types descr' sorts;
     val branchT = if null branchTs then HOLogic.unitT
       else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
-    val arities = remove (op =) 0 (get_arities descr');
+    val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
     val unneeded_vars =
       subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
     val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val (newTs, oldTs) = chop (length (hd descr)) recTs;
     val sumT = if null leafTs then HOLogic.unitT
       else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs;
@@ -143,27 +140,27 @@
 
     (************** generate introduction rules for representing set **********)
 
-    val _ = message config "Constructing representing sets ...";
+    val _ = Datatype_Aux.message config "Constructing representing sets ...";
 
     (* make introduction rule for a single constructor *)
 
     fun make_intr s n (i, (_, cargs)) =
       let
         fun mk_prem dt (j, prems, ts) =
-          (case strip_dtyp dt of
-            (dts, DtRec k) =>
+          (case Datatype_Aux.strip_dtyp dt of
+            (dts, Datatype_Aux.DtRec k) =>
               let
-                val Ts = map (typ_of_dtyp descr' sorts) dts;
+                val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) dts;
                 val free_t =
-                  app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
+                  Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
               in (j + 1, list_all (map (pair "x") Ts,
                   HOLogic.mk_Trueprop
                     (Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems,
                 mk_lim free_t Ts :: ts)
               end
           | _ =>
-              let val T = typ_of_dtyp descr' sorts dt
-              in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
+              let val T = Datatype_Aux.typ_of_dtyp descr' sorts dt
+              in (j + 1, prems, (Leaf $ mk_inj T (Datatype_Aux.mk_Free "x" T j))::ts)
               end);
 
         val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
@@ -221,17 +218,18 @@
     fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
       let
         fun constr_arg dt (j, l_args, r_args) =
-          let val T = typ_of_dtyp descr' sorts dt;
-              val free_t = mk_Free "x" T j
-          in (case (strip_dtyp dt, strip_type T) of
-              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
+          let
+            val T = Datatype_Aux.typ_of_dtyp descr' sorts dt;
+            val free_t = Datatype_Aux.mk_Free "x" T j;
+          in (case (Datatype_Aux.strip_dtyp dt, strip_type T) of
+              ((_, Datatype_Aux.DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
                 (Const (nth all_rep_names m, U --> Univ_elT) $
-                   app_bnds free_t (length Us)) Us :: r_args)
+                   Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args)
             | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
           end;
 
         val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
-        val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
+        val constrT = (map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs) ---> T;
         val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
         val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
         val lhs = list_comb (Const (cname, constrT), l_args);
@@ -276,7 +274,7 @@
 
     (*********** isomorphisms for new types (introduced by typedef) ***********)
 
-    val _ = message config "Proving isomorphism properties ...";
+    val _ = Datatype_Aux.message config "Proving isomorphism properties ...";
 
     val newT_iso_axms = map (fn (_, (_, td)) =>
       (collect_simp (#Abs_inverse td), #Rep_inverse td,
@@ -300,7 +298,7 @@
 
     fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
       let
-        val argTs = map (typ_of_dtyp descr' sorts) cargs;
+        val argTs = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
         val T = nth recTs k;
         val rep_name = nth all_rep_names k;
         val rep_const = Const (rep_name, T --> Univ_elT);
@@ -308,23 +306,23 @@
 
         fun process_arg ks' dt (i2, i2', ts, Ts) =
           let
-            val T' = typ_of_dtyp descr' sorts dt;
+            val T' = Datatype_Aux.typ_of_dtyp descr' sorts dt;
             val (Us, U) = strip_type T'
-          in (case strip_dtyp dt of
-              (_, DtRec j) => if member (op =) ks' j then
-                  (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
-                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
+          in (case Datatype_Aux.strip_dtyp dt of
+              (_, Datatype_Aux.DtRec j) => if member (op =) ks' j then
+                  (i2 + 1, i2' + 1, ts @ [mk_lim (Datatype_Aux.app_bnds
+                     (Datatype_Aux.mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
                    Ts @ [Us ---> Univ_elT])
                 else
                   (i2 + 1, i2', ts @ [mk_lim
                      (Const (nth all_rep_names j, U --> Univ_elT) $
-                        app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
-            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
+                        Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" T' i2) (length Us)) Us], Ts)
+            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (Datatype_Aux.mk_Free "x" T' i2)], Ts))
           end;
 
         val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []);
-        val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
-        val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
+        val xs = map (uncurry (Datatype_Aux.mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
+        val ys = map (uncurry (Datatype_Aux.mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
         val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
 
         val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []);
@@ -383,9 +381,9 @@
             val f = Free ("f", Ts ---> U)
           in Skip_Proof.prove_global thy [] [] (Logic.mk_implies
             (HOLogic.mk_Trueprop (HOLogic.list_all
-               (map (pair "x") Ts, S $ app_bnds f i)),
+               (map (pair "x") Ts, S $ Datatype_Aux.app_bnds f i)),
              HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
-               r $ (a $ app_bnds f i)), f))))
+               r $ (a $ Datatype_Aux.app_bnds f i)), f))))
             (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
                REPEAT (etac allE 1), rtac thm 1, atac 1])
           end
@@ -407,9 +405,9 @@
             val Rep_t = Const (nth all_rep_names i, T --> Univ_elT);
             val rep_set_name = nth rep_set_names i
           in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
-                HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
-                  HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
-              Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i))
+                HOLogic.mk_eq (Rep_t $ Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $
+                  HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)),
+              Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i))
           end;
 
         val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
@@ -419,11 +417,11 @@
           map (fn r => r RS @{thm injD}) inj_thms;
 
         val inj_thm = Skip_Proof.prove_global thy5 [] []
-          (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
-            [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+          (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl1)) (fn _ => EVERY
+            [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
              REPEAT (EVERY
                [rtac allI 1, rtac impI 1,
-                exh_tac (exh_thm_of dt_info) 1,
+                Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
                 REPEAT (EVERY
                   [hyp_subst_tac 1,
                    rewrite_goals_tac rewrites,
@@ -440,17 +438,17 @@
                              Lim_inject :: inj_thms') @ fun_congs) 1),
                          atac 1]))])])])]);
 
-        val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
+        val inj_thms'' = map (fn r => r RS datatype_injI) (Datatype_Aux.split_conj_thm inj_thm);
 
         val elem_thm = 
-            Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
-              (fn _ =>
-               EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
-                rewrite_goals_tac rewrites,
-                REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
-                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
+          Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj ind_concl2))
+            (fn _ =>
+             EVERY [(Datatype_Aux.indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+              rewrite_goals_tac rewrites,
+              REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
+                ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
 
-      in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
+      in (inj_thms'' @ inj_thms, elem_thms @ (Datatype_Aux.split_conj_thm elem_thm))
       end;
 
     val (iso_inj_thms_unfolded, iso_elem_thms) =
@@ -463,14 +461,14 @@
     fun mk_iso_t (((set_name, iso_name), i), T) =
       let val isoT = T --> Univ_elT
       in HOLogic.imp $ 
-        (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
+        (Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
           (if i < length newTs then HOLogic.true_const
-           else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
+           else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
              Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
                Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
       end;
 
-    val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
+    val iso_t = HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (map mk_iso_t
       (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
 
     (* all the theorems are proved by one single simultaneous induction *)
@@ -479,9 +477,9 @@
       iso_inj_thms_unfolded;
 
     val iso_thms = if length descr = 1 then [] else
-      drop (length newTs) (split_conj_thm
+      drop (length newTs) (Datatype_Aux.split_conj_thm
         (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
-           [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+           [(Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
             rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
               Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
@@ -502,7 +500,7 @@
 
     (******************* freeness theorems for constructors *******************)
 
-    val _ = message config "Proving freeness of constructors ...";
+    val _ = Datatype_Aux.message config "Proving freeness of constructors ...";
 
     (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
     
@@ -566,12 +564,12 @@
     val ((constr_inject', distinct_thms'), thy6) =
       thy5
       |> Sign.parent_path
-      |> store_thmss "inject" new_type_names constr_inject
-      ||>> store_thmss "distinct" new_type_names distinct_thms;
+      |> Datatype_Aux.store_thmss "inject" new_type_names constr_inject
+      ||>> Datatype_Aux.store_thmss "distinct" new_type_names distinct_thms;
 
     (*************************** induction theorem ****************************)
 
-    val _ = message config "Proving induction rule for datatypes ...";
+    val _ = Datatype_Aux.message config "Proving induction rule for datatypes ...";
 
     val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
       (map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded);
@@ -580,7 +578,7 @@
     fun mk_indrule_lemma ((i, _), T) (prems, concls) =
       let
         val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $
-          mk_Free "x" T i;
+          Datatype_Aux.mk_Free "x" T i;
 
         val Abs_t = if i < length newTs then
             Const (Sign.intern_const thy6
@@ -589,10 +587,13 @@
               [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $
             HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT)
 
-      in (prems @ [HOLogic.imp $
+      in
+        (prems @
+          [HOLogic.imp $
             (Const (nth rep_set_names i, UnivT') $ Rep_t) $
-              (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
-          concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
+              (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
+         concls @
+          [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i])
       end;
 
     val (indrule_lemma_prems, indrule_lemma_concls) =
@@ -602,8 +603,8 @@
 
     val indrule_lemma = Skip_Proof.prove_global thy6 [] []
       (Logic.mk_implies
-        (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
-         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
+        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
+         HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY
            [REPEAT (etac conjE 1),
             REPEAT (EVERY
               [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
@@ -619,7 +620,7 @@
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn {prems, ...} => EVERY
         [rtac indrule_lemma' 1,
-         (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
+         (Datatype_Aux.indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms 1),
             simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
@@ -680,7 +681,7 @@
               | vs => error ("Extra type variables on rhs: " ^ commas vs));
             val c = Sign.full_name_path tmp_thy tname' cname;
           in
-            (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
+            (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],
               constr_syntax' @ [(cname, mx')], sorts'')
           end handle ERROR msg => cat_error msg
            ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
@@ -691,7 +692,7 @@
       in
         case duplicates (op =) (map fst constrs') of
           [] =>
-            (dts' @ [(i, (Sign.full_name tmp_thy tname, map DtTFree tvs, constrs'))],
+            (dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
               constr_syntax @ [constr_syntax'], sorts', i + 1)
         | dups => error ("Duplicate constructors " ^ commas dups ^
              " in datatype " ^ quote (Binding.str_of tname))
@@ -701,12 +702,14 @@
       fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
     val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
     val dt_info = Datatype_Data.get_all thy;
-    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
-    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
-      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
-      else reraise exn;
+    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
+    val _ =
+      Datatype_Aux.check_nonempty descr
+        handle (exn as Datatype_Aux.Datatype_Empty s) =>
+          if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
+          else reraise exn;
 
-    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
+    val _ = Datatype_Aux.message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
 
   in
     thy
@@ -718,7 +721,7 @@
   end;
 
 val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
-val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ default_config;
+val datatype_cmd = snd ooo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config;
 
 local
 
@@ -745,4 +748,7 @@
 
 end;
 
+
+open Datatype_Data;
+
 end;
diff -r 8a765db7e0f8 -r 25df154b8ffc src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Dec 30 23:42:06 2010 +0100
@@ -35,16 +35,15 @@
 structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
 struct
 
-open Datatype_Aux;
-
 (************************ case distinction theorems ***************************)
 
-fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : Datatype_Aux.config)
+    new_type_names descr sorts induct case_names_exhausts thy =
   let
-    val _ = message config "Proving case distinction theorems ...";
+    val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
 
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val newTs = take (length (hd descr)) recTs;
 
     val {maxidx, ...} = rep_thm induct;
@@ -60,7 +59,7 @@
         val cert = cterm_of thy;
         val insts' = (map cert induct_Ps) ~~ (map cert insts);
         val induct' = refl RS ((nth
-          (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
+          (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
 
       in
         Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
@@ -75,22 +74,23 @@
       (newTs ~~ Datatype_Prop.make_casedists descr sorts)
   in
     thy
-    |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
+    |> Datatype_Aux.store_thms_atts "exhaust" new_type_names
+      (map single case_names_exhausts) casedist_thms
   end;
 
 
 (*************************** primrec combinators ******************************)
 
-fun prove_primrec_thms (config : config) new_type_names descr sorts
+fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr sorts
     injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
   let
-    val _ = message config "Constructing primrec combinators ...";
+    val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
 
     val big_name = space_implode "_" new_type_names;
     val thy0 = Sign.add_path big_name thy;
 
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = take (length (hd descr)) recTs;
 
@@ -108,7 +108,7 @@
     val rec_set_Ts = map (fn (T1, T2) =>
       reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
 
-    val rec_fns = map (uncurry (mk_Free "f"))
+    val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
     val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
       (rec_set_names' ~~ rec_set_Ts);
@@ -120,21 +120,21 @@
     fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
       let
         fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
-          let val free1 = mk_Free "x" U j
-          in (case (strip_dtyp dt, strip_type U) of
-             ((_, DtRec m), (Us, _)) =>
+          let val free1 = Datatype_Aux.mk_Free "x" U j
+          in (case (Datatype_Aux.strip_dtyp dt, strip_type U) of
+             ((_, Datatype_Aux.DtRec m), (Us, _)) =>
                let
-                 val free2 = mk_Free "y" (Us ---> nth rec_result_Ts m) k;
+                 val free2 = Datatype_Aux.mk_Free "y" (Us ---> nth rec_result_Ts m) k;
                  val i = length Us
                in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
                      (map (pair "x") Us, nth rec_sets' m $
-                       app_bnds free1 i $ app_bnds free2 i)) :: prems,
+                       Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
                    free1::t1s, free2::t2s)
                end
            | _ => (j + 1, k, prems, free1::t1s, t2s))
           end;
 
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
         val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
 
       in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
@@ -160,7 +160,7 @@
 
     (* prove uniqueness and termination of primrec combinators *)
 
-    val _ = message config "Proving termination and uniqueness of primrec functions ...";
+    val _ = Datatype_Aux.message config "Proving termination and uniqueness of primrec functions ...";
 
     fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
       let
@@ -175,7 +175,7 @@
 
         fun mk_unique_constr_tac n (cname, cargs) (tac, intr::intrs, j) =
           let
-            val k = length (filter is_rec_type cargs)
+            val k = length (filter Datatype_Aux.is_rec_type cargs)
 
           in (EVERY [DETERM tac,
                 REPEAT (etac ex1E 1), rtac ex1I 1,
@@ -201,7 +201,7 @@
       let
         val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
           Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
-            absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
+            absfree ("y", T2, set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
               (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
         val cert = cterm_of thy1
         val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
@@ -212,8 +212,9 @@
            (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
               THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
 
-      in split_conj_thm (Skip_Proof.prove_global thy1 [] []
-        (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
+      in
+        Datatype_Aux.split_conj_thm (Skip_Proof.prove_global thy1 [] []
+          (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts)) (K tac))
       end;
 
     val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
@@ -247,7 +248,7 @@
 
     (* prove characteristic equations for primrec combinators *)
 
-    val _ = message config "Proving characteristic theorems for primrec combinators ..."
+    val _ = Datatype_Aux.message config "Proving characteristic theorems for primrec combinators ...";
 
     val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
       (fn _ => EVERY
@@ -256,8 +257,7 @@
          resolve_tac rec_unique_thms 1,
          resolve_tac rec_intrs 1,
          REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
-           (Datatype_Prop.make_primrecs new_type_names descr sorts thy2)
-
+           (Datatype_Prop.make_primrecs new_type_names descr sorts thy2);
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
@@ -270,24 +270,25 @@
 
 (***************************** case combinators *******************************)
 
-fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : Datatype_Aux.config)
+    new_type_names descr sorts reccomb_names primrec_thms thy =
   let
-    val _ = message config "Proving characteristic theorems for case combinators ...";
+    val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
 
     val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
 
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
-    fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
+    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
 
     val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
       let
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val Ts' = map mk_dummyT (filter is_rec_type cargs)
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
       in Const (@{const_name undefined}, Ts @ Ts' ---> T')
       end) constrs) descr';
 
@@ -299,11 +300,11 @@
         let
           val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
             let
-              val Ts = map (typ_of_dtyp descr' sorts) cargs;
-              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
-              val frees' = map2 (mk_Free "x") Ts' (1 upto length Ts');
+              val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+              val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
+              val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
               val frees = take (length cargs) frees';
-              val free = mk_Free "f" (Ts ---> T') j
+              val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j
             in
              (free, list_abs_free (map dest_Free frees',
                list_comb (free, frees)))
@@ -335,20 +336,20 @@
     thy2
     |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
     |> Sign.parent_path
-    |> store_thmss "cases" new_type_names case_thms
+    |> Datatype_Aux.store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
   end;
 
 
 (******************************* case splitting *******************************)
 
-fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
-    casedist_thms case_thms thy =
+fun prove_split_thms (config : Datatype_Aux.config)
+    new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy =
   let
-    val _ = message config "Proving equations for case splitting ...";
+    val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
 
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val newTs = take (length (hd descr)) recTs;
 
     fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
@@ -373,8 +374,8 @@
 
   in
     thy
-    |> store_thms "split" new_type_names split_thms
-    ||>> store_thms "split_asm" new_type_names split_asm_thms
+    |> Datatype_Aux.store_thms "split" new_type_names split_thms
+    ||>> Datatype_Aux.store_thms "split_asm" new_type_names split_asm_thms
     |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   end;
 
@@ -387,13 +388,14 @@
     val weak_case_congs = map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs
       new_type_names descr sorts thy)
 
-  in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end;
+  in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
 
 (************************* additional theorems for TFL ************************)
 
-fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : Datatype_Aux.config)
+    new_type_names descr sorts casedist_thms thy =
   let
-    val _ = message config "Proving additional theorems for TFL ...";
+    val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
 
     fun prove_nchotomy (t, exhaustion) =
       let
@@ -404,14 +406,14 @@
       in 
         Skip_Proof.prove_global thy [] [] t (fn _ =>
           EVERY [rtac allI 1,
-           exh_tac (K exhaustion) 1,
+           Datatype_Aux.exh_tac (K exhaustion) 1,
            ALLGOALS (fn i => tac i (i-1))])
       end;
 
     val nchotomys =
       map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms)
 
-  in thy |> store_thms "nchotomy" new_type_names nchotomys end;
+  in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
 
 fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
   let
@@ -437,6 +439,9 @@
     val case_congs = map prove_case_cong (Datatype_Prop.make_case_congs
       new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
 
-  in thy |> store_thms "case_cong" new_type_names case_congs end;
+  in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
+
+
+open Datatype_Aux;
 
 end;
diff -r 8a765db7e0f8 -r 25df154b8ffc src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 30 23:42:06 2010 +0100
@@ -37,8 +37,6 @@
 structure Datatype_Data: DATATYPE_DATA =
 struct
 
-open Datatype_Aux;
-
 (** theory data **)
 
 (* data management *)
@@ -46,9 +44,9 @@
 structure DatatypesData = Theory_Data
 (
   type T =
-    {types: info Symtab.table,
-     constrs: (string * info) list Symtab.table,
-     cases: info Symtab.table};
+    {types: Datatype_Aux.info Symtab.table,
+     constrs: (string * Datatype_Aux.info) list Symtab.table,
+     cases: Datatype_Aux.info Symtab.table};
 
   val empty =
     {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
@@ -85,7 +83,7 @@
 
 val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
 
-fun register (dt_infos : (string * info) list) =
+fun register (dt_infos : (string * Datatype_Aux.info) list) =
   DatatypesData.map (fn {types, constrs, cases} =>
     {types = types |> fold Symtab.update dt_infos,
      constrs = constrs |> fold (fn (constr, dtname_info) =>
@@ -116,13 +114,15 @@
 
     val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
     val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
-      o dest_DtTFree) dtys;
+      o Datatype_Aux.dest_DtTFree) dtys;
 
-    fun is_DtTFree (DtTFree _) = true
+    fun is_DtTFree (Datatype_Aux.DtTFree _) = true
       | is_DtTFree _ = false
     val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
-    val protoTs as (dataTs, _) = chop k descr
-      |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
+    val protoTs as (dataTs, _) =
+      chop k descr
+      |> (pairself o map)
+        (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
     
     val tycos = map fst dataTs;
     val _ = if eq_set (op =) (tycos, raw_tycos) then ()
@@ -133,7 +133,7 @@
 
     val names = map Long_Name.base_name (the_default tycos (#alt_names info));
     val (auxnames, _) = Name.make_context names
-      |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
+      |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us;
     val prefix = space_implode "_" names;
 
   in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
@@ -186,11 +186,11 @@
 
 local
 
-fun dt_recs (DtTFree _) = []
-  | dt_recs (DtType (_, dts)) = maps dt_recs dts
-  | dt_recs (DtRec i) = [i];
+fun dt_recs (Datatype_Aux.DtTFree _) = []
+  | dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts
+  | dt_recs (Datatype_Aux.DtRec i) = [i];
 
-fun dt_cases (descr: descr) (_, args, constrs) =
+fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) =
   let
     fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
     val bnames = map the_bname (distinct (op =) (maps dt_recs args));
@@ -264,7 +264,7 @@
 (** abstract theory extensions relative to a datatype characterisation **)
 
 structure Datatype_Interpretation = Interpretation
-  (type T = config * string list val eq: T * T -> bool = eq_snd op =);
+  (type T = Datatype_Aux.config * string list val eq: T * T -> bool = eq_snd op =);
 fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
 
 fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
@@ -297,7 +297,9 @@
     val thy2 = thy1 |> Theory.checkpoint;
     val flat_descr = flat descr;
     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
-    val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
+    val _ =
+      Datatype_Aux.message config
+        ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
 
     val (exhaust, thy3) = Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
       descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
@@ -305,7 +307,7 @@
       descr sorts exhaust thy3;
     val ((rec_names, rec_rewrites), thy5) = Datatype_Abs_Proofs.prove_primrec_thms
       config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
-      inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts))
+      inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr sorts))
       induct thy4;
     val ((case_rewrites, case_names), thy6) = Datatype_Abs_Proofs.prove_case_thms
       config new_type_names descr sorts rec_names rec_rewrites thy5;
@@ -363,8 +365,8 @@
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
     val (((inject, distinct), [induct]), thy2) =
       thy1
-      |> store_thmss "inject" new_type_names raw_inject
-      ||>> store_thmss "distinct" new_type_names raw_distinct
+      |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject
+      ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct
       ||>> Global_Theory.add_thms
         [((prfx (Binding.name "induct"), raw_induct),
           [mk_case_names_induct descr])];
@@ -411,11 +413,11 @@
 
     val cs = map (apsnd (map norm_constr)) raw_cs;
     val dtyps_of_typ =
-      map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
+      map (Datatype_Aux.dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
     val dt_names = map fst cs;
 
     fun mk_spec (i, (tyco, constr)) = (i, (tyco,
-      map (DtTFree o fst) vs,
+      map (Datatype_Aux.DtTFree o fst) vs,
       (map o apsnd) dtyps_of_typ constr))
     val descr = map_index mk_spec cs;
     val injs = Datatype_Prop.make_injs [descr] vs;
@@ -441,7 +443,7 @@
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global Datatype_Aux.default_config (K I);
 
 
 
@@ -463,4 +465,7 @@
       >> (fn (alt_names, ts) =>
         Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
 
+
+open Datatype_Aux;
+
 end;
diff -r 8a765db7e0f8 -r 25df154b8ffc src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Dec 30 23:42:06 2010 +0100
@@ -35,8 +35,6 @@
 structure Datatype_Prop : DATATYPE_PROP =
 struct
 
-open Datatype_Aux;
-
 fun indexify_names names =
   let
     fun index (x :: xs) tab =
@@ -63,7 +61,7 @@
     fun make_inj T (cname, cargs) =
       if null cargs then I else
         let
-          val Ts = map (typ_of_dtyp descr' sorts) cargs;
+          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
           val constr_t = Const (cname, Ts ---> T);
           val tnames = make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
@@ -75,7 +73,7 @@
         end;
   in
     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
-      (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts))
+      (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
   end;
 
 
@@ -84,10 +82,10 @@
 fun make_distincts descr sorts =
   let
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val newTs = take (length (hd descr)) recTs;
 
-    fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
+    fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
 
     fun make_distincts' _ [] = []
       | make_distincts' T ((cname, cargs)::constrs) =
@@ -117,8 +115,9 @@
 fun make_ind descr sorts =
   let
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
-    val pnames = if length descr' = 1 then ["P"]
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val pnames =
+      if length descr' = 1 then ["P"]
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
 
     fun make_pred i T =
@@ -129,15 +128,18 @@
       let
         fun mk_prem ((dt, s), T) =
           let val (Us, U) = strip_type T
-          in list_all (map (pair "x") Us, HOLogic.mk_Trueprop
-            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
+          in
+            list_all (map (pair "x") Us,
+              HOLogic.mk_Trueprop
+                (make_pred (Datatype_Aux.body_index dt) U $
+                  Datatype_Aux.app_bnds (Free (s, T)) (length Us)))
           end;
 
-        val recs = filter is_rec_type cargs;
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val recTs' = map (typ_of_dtyp descr' sorts) recs;
+        val recs = filter Datatype_Aux.is_rec_type cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
         val tnames = Name.variant_list pnames (make_tnames Ts);
-        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+        val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
         val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
 
@@ -163,7 +165,7 @@
 
     fun make_casedist_prem T (cname, cargs) =
       let
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
         val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees
       in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
@@ -176,7 +178,10 @@
       in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
       end
 
-  in map2 make_casedist (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts)) end;
+  in
+    map2 make_casedist (hd descr)
+      (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
+  end;
 
 (*************** characteristic equations for primrec combinator **************)
 
@@ -190,11 +195,11 @@
     val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let
-          val Ts = map (typ_of_dtyp descr' sorts) cargs;
-          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+          val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
 
           fun mk_argT (dt, T) =
-            binder_types T ---> List.nth (rec_result_Ts, body_index dt);
+            binder_types T ---> List.nth (rec_result_Ts, Datatype_Aux.body_index dt);
 
           val argTs = Ts @ map mk_argT recs
         in argTs ---> List.nth (rec_result_Ts, i)
@@ -205,12 +210,12 @@
 fun make_primrecs new_type_names descr sorts thy =
   let
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
 
     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
 
-    val rec_fns = map (uncurry (mk_Free "f"))
+    val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f"))
       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
 
     val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
@@ -224,18 +229,18 @@
 
     fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =
       let
-        val recs = filter is_rec_type cargs;
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val recTs' = map (typ_of_dtyp descr' sorts) recs;
+        val recs = filter Datatype_Aux.is_rec_type cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
         val tnames = make_tnames Ts;
-        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+        val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
         val frees = map Free (tnames ~~ Ts);
         val frees' = map Free (rec_tnames ~~ recTs');
 
         fun mk_reccomb ((dt, T), t) =
           let val (Us, U) = strip_type T
           in list_abs (map (pair "x") Us,
-            List.nth (reccombs, body_index dt) $ app_bnds t (length Us))
+            List.nth (reccombs, Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
           end;
 
         val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
@@ -256,14 +261,14 @@
 fun make_case_combs new_type_names descr sorts thy fname =
   let
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
-        let val Ts = map (typ_of_dtyp descr' sorts) cargs
+        let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs
         in Ts ---> T' end) constrs) (hd descr);
 
     val case_names = map (fn s =>
@@ -271,7 +276,7 @@
   in
     map (fn ((name, Ts), T) => list_comb
       (Const (name, Ts @ [T] ---> T'),
-        map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
+        map (uncurry (Datatype_Aux.mk_Free fname)) (Ts ~~ (1 upto length Ts))))
           (case_names ~~ case_fn_Ts ~~ newTs)
   end;
 
@@ -280,12 +285,12 @@
 fun make_cases new_type_names descr sorts thy =
   let
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val newTs = take (length (hd descr)) recTs;
 
     fun make_case T comb_t ((cname, cargs), f) =
       let
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
         val frees = map Free ((make_tnames Ts) ~~ Ts)
       in HOLogic.mk_Trueprop (HOLogic.mk_eq
         (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
@@ -303,7 +308,7 @@
 fun make_splits new_type_names descr sorts thy =
   let
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
@@ -316,7 +321,7 @@
 
         fun process_constr ((cname, cargs), f) (t1s, t2s) =
           let
-            val Ts = map (typ_of_dtyp descr' sorts) cargs;
+            val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
             val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
             val eqn = HOLogic.mk_eq (Free ("x", T),
               list_comb (Const (cname, Ts ---> T), frees));
@@ -330,8 +335,8 @@
         val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
         val lhs = P $ (comb_t $ Free ("x", T))
       in
-        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
-         HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ mk_disj t2s)))
+        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Datatype_Aux.mk_conj t1s)),
+         HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Datatype_Aux.mk_disj t2s)))
       end
 
   in map make_split ((hd descr) ~~ newTs ~~
@@ -415,12 +420,12 @@
 fun make_nchotomys descr sorts =
   let
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val newTs = take (length (hd descr)) recTs;
 
     fun mk_eqn T (cname, cargs) =
       let
-        val Ts = map (typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
         val tnames = Name.variant_list ["v"] (make_tnames Ts);
         val frees = tnames ~~ Ts
       in
@@ -430,8 +435,11 @@
       end
 
   in map (fn ((_, (_, _, constrs)), T) =>
-    HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, mk_disj (map (mk_eqn T) constrs))))
+    HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
       (hd descr ~~ newTs)
   end;
 
+
+open Datatype_Aux;
+
 end;
diff -r 8a765db7e0f8 -r 25df154b8ffc src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Dec 30 23:42:06 2010 +0100
@@ -14,8 +14,6 @@
 structure Datatype_Realizer : DATATYPE_REALIZER =
 struct
 
-open Datatype_Aux;
-
 fun subsets i j =
   if i <= j then
     let val is = subsets (i+1) j
@@ -30,9 +28,9 @@
 fun tname_of (Type (s, _)) = s
   | tname_of _ = "";
 
-fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
+fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
   let
-    val recTs = get_rec_types descr sorts;
+    val recTs = Datatype_Aux.get_rec_types descr sorts;
     val pnames = if length descr = 1 then ["P"]
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
 
@@ -51,16 +49,16 @@
     val (prems, rec_fns) = split_list (flat (fst (fold_map
       (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
         let
-          val Ts = map (typ_of_dtyp descr sorts) cargs;
+          val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
           val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
-          val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
+          val recs = filter (Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
           val frees = tnames ~~ Ts;
 
           fun mk_prems vs [] =
                 let
                   val rT = nth (rec_result_Ts) i;
                   val vs' = filter_out is_unit vs;
-                  val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
+                  val f = Datatype_Aux.mk_Free "f" (map fastype_of vs' ---> rT) j;
                   val f' = Envir.eta_contract (list_abs_free
                     (map dest_Free vs, if member (op =) is i then list_comb (f, vs')
                       else HOLogic.unit));
@@ -69,7 +67,7 @@
                 end
             | mk_prems vs (((dt, s), T) :: ds) =
                 let
-                  val k = body_index dt;
+                  val k = Datatype_Aux.body_index dt;
                   val (Us, U) = strip_type T;
                   val i = length Us;
                   val rT = nth (rec_result_Ts) k;
@@ -77,8 +75,8 @@
                   val (p, f) = mk_prems (vs @ [r]) ds
                 in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
                   (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
-                    (make_pred k rT U (app_bnds r i)
-                      (app_bnds (Free (s, T)) i))), p)), f)
+                    (make_pred k rT U (Datatype_Aux.app_bnds r i)
+                      (Datatype_Aux.app_bnds (Free (s, T)) i))), p)), f)
                 end
 
         in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
@@ -154,7 +152,8 @@
   in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
 
 
-fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaust, ...} : info) thy =
+fun make_casedists sorts
+    ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
   let
     val cert = cterm_of thy;
     val rT = TFree ("'P", HOLogic.typeS);
@@ -162,7 +161,7 @@
 
     fun make_casedist_prem T (cname, cargs) =
       let
-        val Ts = map (typ_of_dtyp descr sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
         val frees = Name.variant_list ["P", "y"] (Datatype_Prop.make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
         val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
@@ -173,7 +172,7 @@
       end;
 
     val SOME (_, _, constrs) = AList.lookup (op =) descr index;
-    val T = List.nth (get_rec_types descr sorts, index);
+    val T = List.nth (Datatype_Aux.get_rec_types descr sorts, index);
     val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
     val r = Const (case_name, map fastype_of rs ---> T --> rT);
 
@@ -218,7 +217,7 @@
   if ! Proofterm.proofs < 2 then thy
   else
     let
-      val _ = message config "Adding realizers for induction and case analysis ..."
+      val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
       val infos = map (Datatype.the_info thy) names;
       val info :: _ = infos;
     in
diff -r 8a765db7e0f8 -r 25df154b8ffc src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Thu Dec 30 22:34:53 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Thu Dec 30 23:42:06 2010 +0100
@@ -42,7 +42,7 @@
       NONE => Abs ("x", T, HOLogic.zero)
     | SOME t => t);
 
-fun is_poly thy (DtType (name, dts)) =
+fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
       (case Datatype.get_info thy name of
          NONE => false
        | SOME _ => exists (is_poly thy) dts)