# HG changeset patch
# User wenzelm
# Date 1323727601 -3600
# Node ID ff7bdc67e8cb95c413e5819d57615cd3f6016f89
# Parent  08e44ea5ac6932d550aa016a069f2c0799a3b6e7# Parent  843dc212f69e21109416ead15821d5ab7bbe2d96
merged

diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -77,7 +77,6 @@
 type nominal_datatype_info =
   {index : int,
    descr : descr,
-   sorts : (string * sort) list,
    rec_names : string list,
    rec_rewrites : thm list,
    induction : thm,
@@ -100,12 +99,11 @@
 
 (**** make datatype info ****)
 
-fun make_dt_info descr sorts induct reccomb_names rec_thms
+fun make_dt_info descr induct reccomb_names rec_thms
     (i, (((_, (tname, _, _)), distinct), inject)) =
   (tname,
    {index = i,
     descr = descr,
-    sorts = sorts,
     rec_names = reccomb_names,
     rec_rewrites = rec_thms,
     induction = induct,
@@ -245,7 +243,7 @@
     val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
 
     val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
-    fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+    fun nth_dtyp i = typ_of_dtyp descr (DtRec i);
 
     val big_name = space_implode "_" new_type_names;
 
@@ -268,7 +266,7 @@
       let val T = nth_dtyp i
       in map (fn (cname, dts) =>
         let
-          val Ts = map (typ_of_dtyp descr sorts) dts;
+          val Ts = map (typ_of_dtyp descr) dts;
           val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
           val args = map Free (names ~~ Ts);
           val c = Const (cname, Ts ---> T);
@@ -518,7 +516,7 @@
           apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
-    val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
+    val dt_atomTs = distinct op = (map (typ_of_dtyp descr)
       (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
     val dt_atoms = map (fst o dest_Type) dt_atomTs;
 
@@ -528,9 +526,9 @@
           let
             val (dts, dt') = strip_option dt;
             val (dts', dt'') = strip_dtyp dt';
-            val Ts = map (typ_of_dtyp descr sorts) dts;
-            val Us = map (typ_of_dtyp descr sorts) dts';
-            val T = typ_of_dtyp descr sorts dt'';
+            val Ts = map (typ_of_dtyp descr) dts;
+            val Us = map (typ_of_dtyp descr) dts';
+            val T = typ_of_dtyp descr dt'';
             val free = mk_Free "x" (Us ---> T) j;
             val free' = app_bnds free (length Us);
             fun mk_abs_fun T (i, t) =
@@ -756,14 +754,14 @@
       map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
         (constrs ~~ idxss)))) (descr'' ~~ ndescr);
 
-    fun nth_dtyp' i = typ_of_dtyp descr'' sorts (DtRec i);
+    fun nth_dtyp' i = typ_of_dtyp descr'' (DtRec i);
 
     val rep_names = map (fn s =>
       Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
     val abs_names = map (fn s =>
       Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
 
-    val recTs = get_rec_types descr'' sorts;
+    val recTs = get_rec_types descr'';
     val newTs' = take (length new_type_names) recTs';
     val newTs = take (length new_type_names) recTs;
 
@@ -774,17 +772,17 @@
       let
         fun constr_arg (dts, dt) (j, l_args, r_args) =
           let
-            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
+            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' dt) i)
               (dts ~~ (j upto j + length dts - 1))
-            val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+            val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts)
           in
             (j + length dts + 1,
              xs @ x :: l_args,
              fold_rev mk_abs_fun xs
                (case dt of
                   DtRec k => if k < length new_type_names then
-                      Const (nth rep_names k, typ_of_dtyp descr'' sorts dt -->
-                        typ_of_dtyp descr sorts dt) $ x
+                      Const (nth rep_names k, typ_of_dtyp descr'' dt -->
+                        typ_of_dtyp descr dt) $ x
                     else error "nested recursion not (yet) supported"
                 | _ => x) :: r_args)
           end
@@ -866,7 +864,7 @@
 
     (* prove distinctness theorems *)
 
-    val distinct_props = Datatype_Prop.make_distincts descr' sorts;
+    val distinct_props = Datatype_Prop.make_distincts descr';
     val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
       dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
         constr_rep_thmss dist_lemmas;
@@ -902,10 +900,10 @@
 
           fun constr_arg (dts, dt) (j, l_args, r_args) =
             let
-              val Ts = map (typ_of_dtyp descr'' sorts) dts;
+              val Ts = map (typ_of_dtyp descr'') dts;
               val xs = map (fn (T, i) => mk_Free "x" T i)
                 (Ts ~~ (j upto j + length dts - 1))
-              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+              val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts)
             in
               (j + length dts + 1,
                xs @ x :: l_args,
@@ -952,11 +950,11 @@
 
           fun make_inj (dts, dt) (j, args1, args2, eqs) =
             let
-              val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
+              val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
               val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
-              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts);
-              val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+              val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts);
+              val y = mk_Free "y" (typ_of_dtyp descr'' dt) (j + length dts);
             in
               (j + length dts + 1,
                xs @ (x :: args1), ys @ (y :: args2),
@@ -995,9 +993,9 @@
 
           fun process_constr (dts, dt) (j, args1, args2) =
             let
-              val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
+              val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
-              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
+              val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts);
             in
               (j + length dts + 1,
                xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
@@ -1066,7 +1064,7 @@
 
     val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
 
-    val dt_induct_prop = Datatype_Prop.make_ind descr' sorts;
+    val dt_induct_prop = Datatype_Prop.make_ind descr';
     val dt_induct = Goal.prove_global thy8 []
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn {prems, ...} => EVERY
@@ -1163,8 +1161,8 @@
     fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
       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 Ts = map (typ_of_dtyp descr'') cargs;
+        val recTs' = map (typ_of_dtyp descr'') recs;
         val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
         val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
@@ -1416,7 +1414,7 @@
 
     val used = fold Term.add_tfree_namesT recTs [];
 
-    val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
+    val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' used;
 
     val rec_sort = if null dt_atomTs then HOLogic.typeS else
       Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
@@ -1459,7 +1457,7 @@
     fun make_rec_intr T p rec_set ((cname, cargs), idxs)
         (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) =
       let
-        val Ts = map (typ_of_dtyp descr'' sorts) cargs;
+        val Ts = map (typ_of_dtyp descr'') cargs;
         val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
         val frees' = partition_cargs idxs frees;
         val binders = maps fst frees';
@@ -2046,9 +2044,9 @@
              resolve_tac rec_intrs 1,
              REPEAT (solve (prems @ rec_total_thms) prems 1)])
       end) (rec_eq_prems ~~
-        Datatype_Prop.make_primrecs new_type_names descr' sorts thy12);
+        Datatype_Prop.make_primrecs new_type_names descr' thy12);
 
-    val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
+    val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms)
       (descr1 ~~ distinct_thms ~~ inject_thms);
 
     (* FIXME: theorems are stored in database for testing only *)
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -61,7 +61,7 @@
 (** proof of characteristic theorems **)
 
 fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table)
-    descr sorts types_syntax constr_syntax case_names_induct thy =
+    descr types_syntax constr_syntax case_names_induct thy =
   let
     val descr' = flat descr;
     val new_type_names = map (Binding.name_of o fst) types_syntax;
@@ -70,21 +70,20 @@
     val big_rec_name = big_name ^ "_rep_set";
     val rep_set_names' =
       if length descr' = 1 then [big_rec_name]
-      else map (prefix (big_rec_name ^ "_") o string_of_int) (1 upto (length descr'));
+      else map (prefix (big_rec_name ^ "_") o string_of_int) (1 upto length descr');
     val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
 
     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 leafTs' = Datatype_Aux.get_nonrec_types descr';
+    val branchTs = Datatype_Aux.get_branching_types descr';
     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 (Datatype_Aux.get_arities descr');
     val unneeded_vars =
-      subtract (op =) (fold Term.add_tfree_namesT (leafTs' @ branchTs) []) (hd tyvars);
-    val leafTs =
-      leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+      subtract (op =) (fold Term.add_tfreesT (leafTs' @ branchTs) []) (hd tyvars);
+    val leafTs = leafTs' @ map TFree unneeded_vars;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val (newTs, oldTs) = chop (length (hd descr)) recTs;
     val sumT =
       if null leafTs then HOLogic.unitT
@@ -111,8 +110,8 @@
               val Type (_, [T1, T2]) = T;
             in
               if i <= n2
-              then Const (@{const_name Inl}, T1 --> T) $ (mk_inj' T1 n2 i)
-              else Const (@{const_name Inr}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
+              then Const (@{const_name Inl}, T1 --> T) $ mk_inj' T1 n2 i
+              else Const (@{const_name Inr}, T2 --> T) $ mk_inj' T2 (n - n2) (i - n2)
             end;
       in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs) end;
 
@@ -156,7 +155,7 @@
           (case Datatype_Aux.strip_dtyp dt of
             (dts, Datatype_Aux.DtRec k) =>
               let
-                val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) dts;
+                val Ts = map (Datatype_Aux.typ_of_dtyp descr') dts;
                 val free_t =
                   Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
               in
@@ -166,7 +165,7 @@
                 mk_lim free_t Ts :: ts)
               end
           | _ =>
-              let val T = Datatype_Aux.typ_of_dtyp descr' sorts dt
+              let val T = Datatype_Aux.typ_of_dtyp descr' 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, [], []);
@@ -175,7 +174,7 @@
 
     val intr_ts = maps (fn ((_, (_, _, constrs)), rep_set_name) =>
       map (make_intr rep_set_name (length constrs))
-        ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
+        ((1 upto length constrs) ~~ constrs)) (descr' ~~ rep_set_names');
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       thy1
@@ -194,8 +193,7 @@
       |> Sign.parent_path
       |> fold_map
         (fn (((name, mx), tvs), c) =>
-          Typedef.add_typedef_global false NONE
-            (name, map (rpair dummyS) tvs, mx)
+          Typedef.add_typedef_global false NONE (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
@@ -223,7 +221,7 @@
       let
         fun constr_arg dt (j, l_args, r_args) =
           let
-            val T = Datatype_Aux.typ_of_dtyp descr' sorts dt;
+            val T = Datatype_Aux.typ_of_dtyp descr' dt;
             val free_t = Datatype_Aux.mk_Free "x" T j;
           in
             (case (Datatype_Aux.strip_dtyp dt, strip_type T) of
@@ -235,15 +233,15 @@
           end;
 
         val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
-        val constrT = (map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs) ---> T;
+        val constrT = map (Datatype_Aux.typ_of_dtyp descr') 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);
         val rhs = mk_univ_inj r_args n i;
         val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
         val def_name = Long_Name.base_name cname ^ "_def";
-        val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
+        val eqn =
+          HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
         val ([def_thm], thy') =
           thy
           |> Sign.add_consts_i [(cname', constrT, mx)]
@@ -305,7 +303,7 @@
 
     fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
       let
-        val argTs = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val argTs = map (Datatype_Aux.typ_of_dtyp descr') cargs;
         val T = nth recTs k;
         val rep_name = nth all_rep_names k;
         val rep_const = Const (rep_name, T --> Univ_elT);
@@ -313,7 +311,7 @@
 
         fun process_arg ks' dt (i2, i2', ts, Ts) =
           let
-            val T' = Datatype_Aux.typ_of_dtyp descr' sorts dt;
+            val T' = Datatype_Aux.typ_of_dtyp descr' dt;
             val (Us, U) = strip_type T'
           in
             (case Datatype_Aux.strip_dtyp dt of
@@ -556,7 +554,7 @@
       in prove ts end;
 
     val distinct_thms =
-      map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr sorts);
+      map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr);
 
     (* prove injectivity of constructors *)
 
@@ -582,7 +580,7 @@
 
     val constr_inject =
       map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
-        ((Datatype_Prop.make_injs descr sorts) ~~ constr_rep_thms);
+        (Datatype_Prop.make_injs descr ~~ constr_rep_thms);
 
     val ((constr_inject', distinct_thms'), thy6) =
       thy5
@@ -642,7 +640,7 @@
       else map (Free o apfst fst o dest_Var) Ps;
     val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
 
-    val dt_induct_prop = Datatype_Prop.make_ind descr sorts;
+    val dt_induct_prop = Datatype_Prop.make_ind descr;
     val dt_induct =
       Skip_Proof.prove_global thy6 []
       (Logic.strip_imp_prems dt_induct_prop)
@@ -698,7 +696,7 @@
     val _ =
       (case duplicates (op =) (map fst new_dts) of
         [] => ()
-      | dups => error ("Duplicate datatypes: " ^ commas dups));
+      | dups => error ("Duplicate datatypes: " ^ commas_quote dups));
 
     fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
       let
@@ -721,21 +719,28 @@
       in
         (case duplicates (op =) (map fst constrs') of
           [] =>
-            (dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
+            (dts' @ [(i, (Sign.full_name tmp_thy tname, tvs, constrs'))],
               constr_syntax @ [constr_syntax'], sorts', i + 1)
         | dups =>
-            error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname))
+            error ("Duplicate constructors " ^ commas_quote dups ^
+              " in datatype " ^ Binding.print tname))
       end;
 
-    val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
-    val sorts =
-      sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
+    val (dts0, constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
+    val tmp_ctxt' = tmp_ctxt |> fold (Variable.declare_typ o TFree) sorts';
+
+    val dts' = dts0 |> map (fn (i, (name, tvs, cs)) =>
+      let
+        val args = tvs |>
+          map (fn a => Datatype_Aux.DtTFree (a, Proof_Context.default_sort tmp_ctxt' (a, ~1)));
+      in (i, (name, args, cs)) end);
+
     val dt_info = Datatype_Data.get_all thy;
-    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' sorts dt_info dts' i;
+    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' 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)
+          if #strict config then error ("Nonemptiness check failed for datatype " ^ quote s)
           else reraise exn;
 
     val _ =
@@ -743,10 +748,10 @@
         ("Constructing datatype(s) " ^ commas_quote (map (Binding.name_of o #2) dts));
   in
     thy
-    |> representation_proofs config dt_info descr sorts types_syntax constr_syntax
+    |> representation_proofs config dt_info descr types_syntax constr_syntax
       (Datatype_Data.mk_case_names_induct (flat descr))
     |-> (fn (inject, distinct, induct) =>
-      Datatype_Data.derive_datatype_props config dt_names descr sorts induct inject distinct)
+      Datatype_Data.derive_datatype_props config dt_names descr induct inject distinct)
   end;
 
 val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/Datatype/datatype_abs_proofs.ML
     Author:     Stefan Berghofer, TU Muenchen
 
-Datatype package: proofs and defintions independent of concrete
+Datatype package: proofs and definitions independent of concrete
 representation of datatypes  (i.e. requiring only abstract
 properties: injectivity / distinctness of constructors and induction).
 *)
@@ -9,27 +9,21 @@
 signature DATATYPE_ABS_PROOFS =
 sig
   include DATATYPE_COMMON
-  val prove_casedist_thms : config -> string list ->
-    descr list -> (string * sort) list -> thm ->
+  val prove_casedist_thms : config -> string list -> descr list -> thm ->
     attribute list -> theory -> thm list * theory
-  val prove_primrec_thms : config -> string list ->
-    descr list -> (string * sort) list ->
-      (string -> thm list) -> thm list list -> thm list list * thm list list ->
-        thm -> theory -> (string list * thm list) * theory
-  val prove_case_thms : config -> string list ->
-    descr list -> (string * sort) list ->
-      string list -> thm list -> theory -> (thm list list * string list) * theory
-  val prove_split_thms : config -> string list ->
-    descr list -> (string * sort) list ->
-      thm list list -> thm list list -> thm list -> thm list list -> theory ->
-        (thm * thm) list * theory
+  val prove_primrec_thms : config -> string list -> descr list ->
+    (string -> thm list) -> thm list list -> thm list list * thm list list ->
+      thm -> theory -> (string list * thm list) * theory
+  val prove_case_thms : config -> string list -> descr list ->
+    string list -> thm list -> theory -> (thm list list * string list) * theory
+  val prove_split_thms : config -> string list -> descr list ->
+    thm list list -> thm list list -> thm list -> thm list list -> theory ->
+    (thm * thm) list * theory
   val prove_nchotomys : config -> string list -> descr list ->
-    (string * sort) list -> thm list -> theory -> thm list * theory
-  val prove_weak_case_congs : string list -> descr list ->
-    (string * sort) list -> theory -> thm list * theory
-  val prove_case_congs : string list ->
-    descr list -> (string * sort) list ->
-      thm list -> thm list list -> theory -> thm list * theory
+    thm list -> theory -> thm list * theory
+  val prove_weak_case_congs : string list -> descr list -> theory -> thm list * theory
+  val prove_case_congs : string list -> descr list ->
+    thm list -> thm list list -> theory -> thm list * theory
 end;
 
 structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
@@ -38,12 +32,12 @@
 (************************ case distinction theorems ***************************)
 
 fun prove_casedist_thms (config : Datatype_Aux.config)
-    new_type_names descr sorts induct case_names_exhausts thy =
+    new_type_names descr induct case_names_exhausts thy =
   let
     val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
 
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val newTs = take (length (hd descr)) recTs;
 
     val maxidx = Thm.maxidx_of induct;
@@ -75,7 +69,7 @@
       end;
 
     val casedist_thms =
-      map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr sorts);
+      map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr);
   in
     thy
     |> Datatype_Aux.store_thms_atts "exhaust" new_type_names
@@ -85,7 +79,7 @@
 
 (*************************** primrec combinators ******************************)
 
-fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr sorts
+fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr
     injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
   let
     val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
@@ -94,7 +88,7 @@
     val thy0 = Sign.add_path big_name thy;
 
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
 
@@ -103,16 +97,16 @@
     val big_rec_name' = big_name ^ "_rec_set";
     val rec_set_names' =
       if length descr' = 1 then [big_rec_name']
-      else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto (length descr'));
+      else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto length descr');
     val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
 
-    val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr sorts used;
+    val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr used;
 
     val rec_set_Ts =
       map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
 
     val rec_fns =
-      map (uncurry (Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
+      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);
     val rec_sets =
@@ -136,10 +130,10 @@
                         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))
+            | _ => (j + 1, k, prems, free1 :: t1s, t2s))
           end;
 
-        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
         val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], []);
 
       in
@@ -233,7 +227,7 @@
     val reccomb_names =
       map (Sign.full_bname thy1)
         (if length descr' = 1 then [big_reccomb_name]
-         else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto (length descr')));
+         else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'));
     val reccombs =
       map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
         (reccomb_names ~~ recTs ~~ rec_result_Ts);
@@ -268,7 +262,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 thy2);
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
@@ -282,24 +276,24 @@
 (***************************** case combinators *******************************)
 
 fun prove_case_thms (config : Datatype_Aux.config)
-    new_type_names descr sorts reccomb_names primrec_thms thy =
+    new_type_names descr reccomb_names primrec_thms thy =
   let
     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 = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
 
-    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
+    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
 
     val case_dummy_fns =
       map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
         let
-          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
           val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
         in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
 
@@ -312,7 +306,7 @@
           let
             val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
               let
-                val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+                val Ts = map (Datatype_Aux.typ_of_dtyp descr') 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';
@@ -344,7 +338,7 @@
           Skip_Proof.prove_global thy2 [] [] t
             (fn _ =>
               EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
-        (Datatype_Prop.make_cases new_type_names descr sorts thy2);
+        (Datatype_Prop.make_cases new_type_names descr thy2);
   in
     thy2
     |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
@@ -357,12 +351,12 @@
 (******************************* case splitting *******************************)
 
 fun prove_split_thms (config : Datatype_Aux.config)
-    new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy =
+    new_type_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
   let
     val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
 
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val newTs = take (length (hd descr)) recTs;
 
     fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
@@ -380,7 +374,7 @@
 
     val split_thm_pairs =
       map prove_split_thms
-        ((Datatype_Prop.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
+        (Datatype_Prop.make_splits new_type_names descr thy ~~ constr_inject ~~
           dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
 
     val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
@@ -392,21 +386,20 @@
     |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   end;
 
-fun prove_weak_case_congs new_type_names descr sorts thy =
+fun prove_weak_case_congs new_type_names descr thy =
   let
     fun prove_weak_case_cong t =
      Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
        (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1]);
 
     val weak_case_congs =
-      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr sorts thy);
+      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr thy);
 
   in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
 
 (************************* additional theorems for TFL ************************)
 
-fun prove_nchotomys (config : Datatype_Aux.config)
-    new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : Datatype_Aux.config) new_type_names descr casedist_thms thy =
   let
     val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
 
@@ -424,11 +417,11 @@
       end;
 
     val nchotomys =
-      map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms);
+      map prove_nchotomy (Datatype_Prop.make_nchotomys descr ~~ casedist_thms);
 
   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 =
+fun prove_case_congs new_type_names descr nchotomys case_thms thy =
   let
     fun prove_case_cong ((t, nchotomy), case_rewrites) =
       let
@@ -452,7 +445,7 @@
 
     val case_congs =
       map prove_case_cong (Datatype_Prop.make_case_congs
-        new_type_names descr sorts thy ~~ nchotomys ~~ case_thms);
+        new_type_names descr thy ~~ nchotomys ~~ case_thms);
 
   in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
 
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -9,14 +9,13 @@
   type config = {strict : bool, quiet : bool}
   val default_config : config
   datatype dtyp =
-      DtTFree of string
+      DtTFree of string * sort
     | DtType of string * dtyp list
     | DtRec of int
   type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
   type info =
    {index : int,
     descr : descr,
-    sorts : (string * sort) list,
     inject : thm list,
     distinct : thm list,
     induct : thm,
@@ -61,23 +60,22 @@
   val dtyp_of_typ : (string * string list) list -> typ -> dtyp
   val mk_Free : string -> typ -> int -> term
   val is_rec_type : dtyp -> bool
-  val typ_of_dtyp : descr -> (string * sort) list -> dtyp -> typ
-  val dest_DtTFree : dtyp -> string
+  val typ_of_dtyp : descr -> dtyp -> typ
+  val dest_DtTFree : dtyp -> string * sort
   val dest_DtRec : dtyp -> int
   val strip_dtyp : dtyp -> dtyp list * dtyp
   val body_index : dtyp -> int
   val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
-  val get_nonrec_types : descr -> (string * sort) list -> typ list
-  val get_branching_types : descr -> (string * sort) list -> typ list
+  val get_nonrec_types : descr -> typ list
+  val get_branching_types : descr -> typ list
   val get_arities : descr -> int list
-  val get_rec_types : descr -> (string * sort) list -> typ list
-  val interpret_construction : descr -> (string * sort) list
-    -> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
-    -> ((string * typ list) * (string * 'a list) list) list
+  val get_rec_types : descr -> typ list
+  val interpret_construction : descr -> (string * sort) list ->
+    {atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a} ->
+    ((string * typ list) * (string * 'a list) list) list
   val check_nonempty : descr list -> unit
-  val unfold_datatypes :
-    Proof.context -> descr -> (string * sort) list -> info Symtab.table ->
-      descr -> int -> descr list * int
+  val unfold_datatypes : Proof.context -> descr -> info Symtab.table ->
+    descr -> int -> descr list * int
   val find_shortest_path : descr -> int -> (string * int) option
 end;
 
@@ -176,8 +174,8 @@
 (********************** Internal description of datatypes *********************)
 
 datatype dtyp =
-    DtTFree of string
-  | DtType of string * (dtyp list)
+    DtTFree of string * sort
+  | DtType of string * dtyp list
   | DtRec of int;
 
 (* information about datatypes *)
@@ -188,7 +186,6 @@
 type info =
   {index : int,
    descr : descr,
-   sorts : (string * sort) list,
    inject : thm list,
    distinct : thm list,
    induct : thm,
@@ -206,7 +203,7 @@
 
 fun mk_Free s T i = Free (s ^ string_of_int i, T);
 
-fun subst_DtTFree _ substs (T as DtTFree name) = the_default T (AList.lookup (op =) substs name)
+fun subst_DtTFree _ substs (T as DtTFree a) = the_default T (AList.lookup (op =) substs a)
   | subst_DtTFree i substs (DtType (name, ts)) = DtType (name, map (subst_DtTFree i substs) ts)
   | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
 
@@ -239,7 +236,7 @@
       end
   | name_of_typ _ = "";
 
-fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
+fun dtyp_of_typ _ (TFree a) = DtTFree a
   | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
   | dtyp_of_typ new_dts (Type (tname, Ts)) =
       (case AList.lookup (op =) new_dts tname of
@@ -247,29 +244,29 @@
       | SOME vs =>
           if map (try (fst o dest_TFree)) Ts = map SOME vs then
             DtRec (find_index (curry op = tname o fst) new_dts)
-          else error ("Illegal occurrence of recursive type " ^ tname));
+          else error ("Illegal occurrence of recursive type " ^ quote tname));
 
-fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, (the o AList.lookup (op =) sorts) a)
-  | typ_of_dtyp descr sorts (DtRec i) =
+fun typ_of_dtyp descr (DtTFree a) = TFree a
+  | typ_of_dtyp descr (DtRec i) =
       let val (s, ds, _) = the (AList.lookup (op =) descr i)
-      in Type (s, map (typ_of_dtyp descr sorts) ds) end
-  | typ_of_dtyp descr sorts (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr sorts) ds);
+      in Type (s, map (typ_of_dtyp descr) ds) end
+  | typ_of_dtyp descr (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr) ds);
 
 (* find all non-recursive types in datatype description *)
 
-fun get_nonrec_types descr sorts =
-  map (typ_of_dtyp descr sorts) (fold (fn (_, (_, _, constrs)) =>
+fun get_nonrec_types descr =
+  map (typ_of_dtyp descr) (fold (fn (_, (_, _, constrs)) =>
     fold (fn (_, cargs) => union (op =) (filter_out is_rec_type cargs)) constrs) descr []);
 
 (* get all recursive types in datatype description *)
 
-fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
-  Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
+fun get_rec_types descr = map (fn (_ , (s, ds, _)) =>
+  Type (s, map (typ_of_dtyp descr) ds)) descr;
 
 (* get all branching types *)
 
-fun get_branching_types descr sorts =
-  map (typ_of_dtyp descr sorts)
+fun get_branching_types descr =
+  map (typ_of_dtyp descr)
     (fold
       (fn (_, (_, _, constrs)) =>
         fold (fn (_, cargs) => fold (strip_dtyp #> fst #> fold (insert op =)) cargs) constrs)
@@ -286,19 +283,21 @@
 
 fun interpret_construction descr vs {atyp, dtyp} =
   let
-    val typ_of_dtyp = typ_of_dtyp descr vs;
+    val typ_of =
+      typ_of_dtyp descr #>
+      map_atyps (fn TFree (a, _) => TFree (a, the (AList.lookup (op =) vs a)) | T => T);
     fun interpT dT =
       (case strip_dtyp dT of
         (dTs, DtRec l) =>
           let
             val (tyco, dTs', _) = the (AList.lookup (op =) descr l);
-            val Ts = map typ_of_dtyp dTs;
-            val Ts' = map typ_of_dtyp dTs';
+            val Ts = map typ_of dTs;
+            val Ts' = map typ_of dTs';
             val is_proper = forall (can dest_TFree) Ts';
           in dtyp Ts (l, is_proper) (tyco, Ts') end
-      | _ => atyp (typ_of_dtyp dT));
+      | _ => atyp (typ_of dT));
     fun interpC (c, dTs) = (c, map interpT dTs);
-    fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of_dtyp dTs), map interpC cs);
+    fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of dTs), map interpC cs);
   in map interpD descr end;
 
 (* nonemptiness check for datatypes *)
@@ -323,22 +322,23 @@
 (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
 (* need to be unfolded                                         *)
 
-fun unfold_datatypes ctxt orig_descr sorts (dt_info : info Symtab.table) descr i =
+fun unfold_datatypes ctxt orig_descr (dt_info : info Symtab.table) descr i =
   let
     fun typ_error T msg =
       error ("Non-admissible type expression\n" ^
-        Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
+        Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) T) ^ "\n" ^ msg);
 
     fun get_dt_descr T i tname dts =
       (case Symtab.lookup dt_info tname of
         NONE =>
-          typ_error T (tname ^ " is not a datatype - can't use it in nested recursion")
+          typ_error T (quote tname ^ " is not a datatype - can't use it in nested recursion")
       | SOME {index, descr, ...} =>
           let
             val (_, vars, _) = the (AList.lookup (op =) descr index);
             val subst = map dest_DtTFree vars ~~ dts
               handle ListPair.UnequalLengths =>
-                typ_error T ("Type constructor " ^ tname ^ " used with wrong number of arguments");
+                typ_error T ("Type constructor " ^ quote tname ^
+                  " used with wrong number of arguments");
           in
             (i + index,
               map (fn (j, (tn, args, cs)) =>
@@ -359,7 +359,7 @@
                 let
                   val (index, descr) = get_dt_descr T i tname dts;
                   val (descr', i') =
-                    unfold_datatypes ctxt orig_descr sorts dt_info descr (i + length descr);
+                    unfold_datatypes ctxt orig_descr dt_info descr (i + length descr);
                 in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
             | _ => (i, Ts @ [T], descrs))
         end
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -36,10 +36,10 @@
 
 fun ty_info tab sT =
   (case tab sT of
-    SOME ({descr, case_name, index, sorts, ...} : info) =>
+    SOME ({descr, case_name, index, ...} : info) =>
       let
         val (_, (tname, dts, constrs)) = nth descr index;
-        val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
+        val mk_ty = Datatype_Aux.typ_of_dtyp descr;
         val T = Type (tname, map mk_ty dts);
       in
         SOME {case_name = case_name,
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -76,11 +76,11 @@
           | _ => NONE) cos;
     fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
       trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
-    val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
+    val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index);
     fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
       [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
     val distincts =
-      maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
+      maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index));
     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
     val simpset =
       Simplifier.global_context thy
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -7,7 +7,7 @@
 signature DATATYPE_DATA =
 sig
   include DATATYPE_COMMON
-  val derive_datatype_props : config -> string list -> descr list -> (string * sort) list ->
+  val derive_datatype_props : config -> string list -> descr list ->
     thm -> thm list list -> thm list list -> theory -> string list * theory
   val rep_datatype : config -> (string list -> Proof.context -> Proof.context) ->
     term list -> theory -> Proof.state
@@ -69,7 +69,7 @@
 
 fun info_of_constr thy (c, T) =
   let
-    val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
+    val tab = Symtab.lookup_list (#constrs (DatatypesData.get thy)) c;
   in
     (case body_type T of
       Type (tyco, _) => AList.lookup (op =) tab tyco
@@ -109,22 +109,19 @@
 
 fun the_spec thy dtco =
   let
-    val { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
-    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
-    val sorts =
-      map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v)) o Datatype_Aux.dest_DtTFree) dtys;
-    val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos;
-  in (sorts, cos) end;
+    val {descr, index, ...} = the_info thy dtco;
+    val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index);
+    val args = map Datatype_Aux.dest_DtTFree dtys;
+    val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos;
+  in (args, cos) end;
 
 fun the_descr thy (raw_tycos as raw_tyco :: _) =
   let
     val info = the_info thy raw_tyco;
     val descr = #descr info;
 
-    val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
-    val vs =
-      map ((fn v => (v, the (AList.lookup (op =) (#sorts info) v))) o Datatype_Aux.dest_DtTFree)
-        dtys;
+    val (_, dtys, _) = the (AList.lookup (op =) descr (#index info));
+    val vs = map Datatype_Aux.dest_DtTFree dtys;
 
     fun is_DtTFree (Datatype_Aux.DtTFree _) = true
       | is_DtTFree _ = false;
@@ -132,7 +129,7 @@
     val protoTs as (dataTs, _) =
       chop k descr
       |> (pairself o map)
-        (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
+        (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr) dTs));
 
     val tycos = map fst dataTs;
     val _ =
@@ -160,12 +157,12 @@
 
 fun get_constrs thy dtco =
   (case try (the_spec thy) dtco of
-    SOME (sorts, cos) =>
+    SOME (args, cos) =>
       let
         fun subst (v, sort) = TVar ((v, 0), sort);
         fun subst_ty (TFree v) = subst v
           | subst_ty ty = ty;
-        val dty = Type (dtco, map subst sorts);
+        val dty = Type (dtco, map subst args);
         fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
       in SOME (map mk_co cos) end
   | NONE => NONE);
@@ -283,14 +280,13 @@
 );
 fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
 
-fun make_dt_info descr sorts induct inducts rec_names rec_rewrites
+fun make_dt_info descr induct inducts rec_names rec_rewrites
     (index, (((((((((((_, (tname, _, _))), inject), distinct),
       exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
         (split, split_asm))) =
   (tname,
    {index = index,
     descr = descr,
-    sorts = sorts,
     inject = inject,
     distinct = distinct,
     induct = induct,
@@ -306,8 +302,7 @@
     split = split,
     split_asm = split_asm});
 
-fun derive_datatype_props config dt_names descr sorts
-    induct inject distinct thy1 =
+fun derive_datatype_props config dt_names descr induct inject distinct thy1 =
   let
     val thy2 = thy1 |> Theory.checkpoint;
     val flat_descr = flat descr;
@@ -316,32 +311,28 @@
       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;
-    val (nchotomys, thy4) =
-      Datatype_Abs_Proofs.prove_nchotomys config new_type_names
-        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 (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;
-    val (case_congs, thy7) =
-      Datatype_Abs_Proofs.prove_case_congs new_type_names
-        descr sorts nchotomys case_rewrites thy6;
-    val (weak_case_congs, thy8) =
-      Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr sorts thy7;
-    val (splits, thy9) =
-      Datatype_Abs_Proofs.prove_split_thms
-        config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
+    val (exhaust, thy3) = thy2
+      |> Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
+        descr induct (mk_case_names_exhausts flat_descr dt_names);
+    val (nchotomys, thy4) = thy3
+      |> Datatype_Abs_Proofs.prove_nchotomys config new_type_names descr exhaust;
+    val ((rec_names, rec_rewrites), thy5) = thy4
+      |> Datatype_Abs_Proofs.prove_primrec_thms
+        config new_type_names descr (#inject o the o Symtab.lookup (get_all thy4))
+        inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr)) induct;
+    val ((case_rewrites, case_names), thy6) = thy5
+      |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites;
+    val (case_congs, thy7) = thy6
+      |> Datatype_Abs_Proofs.prove_case_congs new_type_names descr nchotomys case_rewrites;
+    val (weak_case_congs, thy8) = thy7
+      |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr;
+    val (splits, thy9) = thy8
+      |> Datatype_Abs_Proofs.prove_split_thms
+        config new_type_names descr inject distinct exhaust case_rewrites;
 
     val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
     val dt_infos = map_index
-      (make_dt_info flat_descr sorts induct inducts rec_names rec_rewrites)
+      (make_dt_info flat_descr induct inducts rec_names rec_rewrites)
       (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
         case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
     val dt_names = map fst dt_infos;
@@ -378,7 +369,7 @@
 
 (** declare existing type as datatype **)
 
-fun prove_rep_datatype config dt_names descr sorts raw_inject half_distinct raw_induct thy1 =
+fun prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct thy1 =
   let
     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     val new_type_names = map Long_Name.base_name dt_names;
@@ -392,7 +383,7 @@
           [mk_case_names_induct descr])];
   in
     thy2
-    |> derive_datatype_props config dt_names [descr] sorts induct inject distinct
+    |> derive_datatype_props config dt_names [descr] induct inject distinct
  end;
 
 fun gen_rep_datatype prep_term config after_qed raw_ts thy =
@@ -441,13 +432,11 @@
     val dt_names = map fst cs;
 
     fun mk_spec (i, (tyco, constr)) =
-      (i, (tyco,
-        map (Datatype_Aux.DtTFree o fst) vs,
-        (map o apsnd) dtyps_of_typ constr));
+      (i, (tyco, map Datatype_Aux.DtTFree vs, (map o apsnd) dtyps_of_typ constr));
     val descr = map_index mk_spec cs;
-    val injs = Datatype_Prop.make_injs [descr] vs;
-    val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs);
-    val ind = Datatype_Prop.make_ind [descr] vs;
+    val injs = Datatype_Prop.make_injs [descr];
+    val half_distincts = map snd (Datatype_Prop.make_distincts [descr]);
+    val ind = Datatype_Prop.make_ind [descr];
     val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
 
     fun after_qed' raw_thms =
@@ -457,7 +446,7 @@
             (*FIXME somehow dubious*)
       in
         Proof_Context.background_theory_result  (* FIXME !? *)
-          (prove_rep_datatype config dt_names descr vs raw_inject half_distinct raw_induct)
+          (prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct)
         #-> after_qed
       end;
   in
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -9,27 +9,18 @@
   include DATATYPE_COMMON
   val indexify_names: string list -> string list
   val make_tnames: typ list -> string list
-  val make_injs : descr list -> (string * sort) list -> term list list
-  val make_distincts : descr list ->
-    (string * sort) list -> (int * term list) list (*no symmetric inequalities*)
-  val make_ind : descr list -> (string * sort) list -> term
-  val make_casedists : descr list -> (string * sort) list -> term list
-  val make_primrec_Ts : descr list -> (string * sort) list ->
-    string list -> typ list * typ list
-  val make_primrecs : string list -> descr list ->
-    (string * sort) list -> theory -> term list
-  val make_cases : string list -> descr list ->
-    (string * sort) list -> theory -> term list list
-  val make_splits : string list -> descr list ->
-    (string * sort) list -> theory -> (term * term) list
-  val make_case_combs : string list -> descr list ->
-    (string * sort) list -> theory -> string -> term list
-  val make_weak_case_congs : string list -> descr list ->
-    (string * sort) list -> theory -> term list
-  val make_case_congs : string list -> descr list ->
-    (string * sort) list -> theory -> term list
-  val make_nchotomys : descr list ->
-    (string * sort) list -> term list
+  val make_injs : descr list -> term list list
+  val make_distincts : descr list -> (int * term list) list (*no symmetric inequalities*)
+  val make_ind : descr list -> term
+  val make_casedists : descr list -> term list
+  val make_primrec_Ts : descr list -> string list -> typ list * typ list
+  val make_primrecs : string list -> descr list -> theory -> term list
+  val make_cases : string list -> descr list -> theory -> term list list
+  val make_splits : string list -> descr list -> theory -> (term * term) list
+  val make_case_combs : string list -> descr list -> theory -> string -> term list
+  val make_weak_case_congs : string list -> descr list -> theory -> term list
+  val make_case_congs : string list -> descr list -> theory -> term list
+  val make_nchotomys : descr list -> term list
 end;
 
 structure Datatype_Prop : DATATYPE_PROP =
@@ -58,14 +49,14 @@
 
 (************************* injectivity of constructors ************************)
 
-fun make_injs descr sorts =
+fun make_injs descr =
   let
     val descr' = flat descr;
     fun make_inj T (cname, cargs) =
       if null cargs then I
       else
         let
-          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
           val constr_t = Const (cname, Ts ---> T);
           val tnames = make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
@@ -78,20 +69,19 @@
         end;
   in
     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
-      (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
+      (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
   end;
 
 
 (************************* distinctness of constructors ***********************)
 
-fun make_distincts descr sorts =
+fun make_distincts descr =
   let
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val newTs = take (length (hd descr)) recTs;
 
-    fun prep_constr (cname, cargs) =
-      (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
+    fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr') cargs);
 
     fun make_distincts' _ [] = []
       | make_distincts' T ((cname, cargs) :: constrs) =
@@ -115,10 +105,10 @@
 
 (********************************* induction **********************************)
 
-fun make_ind descr sorts =
+fun make_ind descr =
   let
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val pnames =
       if length descr' = 1 then ["P"]
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
@@ -139,8 +129,8 @@
           end;
 
         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 Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
+        val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
         val tnames = Name.variant_list pnames (make_tnames Ts);
         val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
@@ -164,13 +154,13 @@
 
 (******************************* case distinction *****************************)
 
-fun make_casedists descr sorts =
+fun make_casedists descr =
   let
     val descr' = flat descr;
 
     fun make_casedist_prem T (cname, cargs) =
       let
-        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
         val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
       in
@@ -186,12 +176,12 @@
 
   in
     map2 make_casedist (hd descr)
-      (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
+      (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
   end;
 
 (*************** characteristic equations for primrec combinator **************)
 
-fun make_primrec_Ts descr sorts used =
+fun make_primrec_Ts descr used =
   let
     val descr' = flat descr;
 
@@ -203,7 +193,7 @@
     val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let
-          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
           val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
 
           fun mk_argT (dt, T) =
@@ -214,13 +204,13 @@
 
   in (rec_result_Ts, reccomb_fn_Ts) end;
 
-fun make_primrecs new_type_names descr sorts thy =
+fun make_primrecs new_type_names descr thy =
   let
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val used = fold Term.add_tfree_namesT recTs [];
 
-    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
+    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr used;
 
     val rec_fns =
       map (uncurry (Datatype_Aux.mk_Free "f"))
@@ -230,7 +220,7 @@
     val reccomb_names =
       map (Sign.intern_const thy)
         (if length descr' = 1 then [big_reccomb_name]
-         else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto (length descr'))));
+         else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr')));
     val reccombs =
       map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
         (reccomb_names ~~ recTs ~~ rec_result_Ts);
@@ -238,8 +228,8 @@
     fun make_primrec T comb_t (cname, cargs) (ts, f :: fs) =
       let
         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 Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
+        val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
         val tnames = make_tnames Ts;
         val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
         val frees = map Free (tnames ~~ Ts);
@@ -266,17 +256,17 @@
 
 (****************** make terms of form  t_case f1 ... fn  *********************)
 
-fun make_case_combs new_type_names descr sorts thy fname =
+fun make_case_combs new_type_names descr thy fname =
   let
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val used = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
-        let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs
+        let val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs
         in Ts ---> T' end) constrs) (hd descr);
 
     val case_names = map (fn s => Sign.intern_const thy (s ^ "_case")) new_type_names;
@@ -289,15 +279,15 @@
 
 (**************** characteristic equations for case combinator ****************)
 
-fun make_cases new_type_names descr sorts thy =
+fun make_cases new_type_names descr thy =
   let
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val newTs = take (length (hd descr)) recTs;
 
     fun make_case T comb_t ((cname, cargs), f) =
       let
-        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
         val frees = map Free ((make_tnames Ts) ~~ Ts);
       in
         HOLogic.mk_Trueprop
@@ -307,16 +297,16 @@
   in
     map (fn (((_, (_, _, constrs)), T), comb_t) =>
       map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
-        ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
+        ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr thy "f"))
   end;
 
 
 (*************************** the "split" - equations **************************)
 
-fun make_splits new_type_names descr sorts thy =
+fun make_splits new_type_names descr thy =
   let
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val used' = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
@@ -329,7 +319,7 @@
 
         fun process_constr ((cname, cargs), f) (t1s, t2s) =
           let
-            val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+            val Ts = map (Datatype_Aux.typ_of_dtyp descr') 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));
             val P' = P $ list_comb (f, frees);
@@ -348,14 +338,14 @@
       end
 
   in
-    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr sorts thy "f")
+    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr thy "f")
   end;
 
 (************************* additional rules for TFL ***************************)
 
-fun make_weak_case_congs new_type_names descr sorts thy =
+fun make_weak_case_congs new_type_names descr thy =
   let
-    val case_combs = make_case_combs new_type_names descr sorts thy "f";
+    val case_combs = make_case_combs new_type_names descr thy "f";
 
     fun mk_case_cong comb =
       let
@@ -382,10 +372,10 @@
  *      (ty_case f1..fn M = ty_case g1..gn M')
  *---------------------------------------------------------------------------*)
 
-fun make_case_congs new_type_names descr sorts thy =
+fun make_case_congs new_type_names descr thy =
   let
-    val case_combs = make_case_combs new_type_names descr sorts thy "f";
-    val case_combs' = make_case_combs new_type_names descr sorts thy "g";
+    val case_combs = make_case_combs new_type_names descr thy "f";
+    val case_combs' = make_case_combs new_type_names descr thy "g";
 
     fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
       let
@@ -423,15 +413,15 @@
  *    !v. (? y1..yi. v = C1 y1..yi) | ... | (? y1..yj. v = Cn y1..yj)
  *---------------------------------------------------------------------------*)
 
-fun make_nchotomys descr sorts =
+fun make_nchotomys descr =
   let
     val descr' = flat descr;
-    val recTs = Datatype_Aux.get_rec_types descr' sorts;
+    val recTs = Datatype_Aux.get_rec_types descr';
     val newTs = take (length (hd descr)) recTs;
 
     fun mk_eqn T (cname, cargs) =
       let
-        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
         val tnames = Name.variant_list ["v"] (make_tnames Ts);
         val frees = tnames ~~ Ts;
       in
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -25,9 +25,9 @@
 fun tname_of (Type (s, _)) = s
   | tname_of _ = "";
 
-fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
+fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
   let
-    val recTs = Datatype_Aux.get_rec_types descr sorts;
+    val recTs = Datatype_Aux.get_rec_types descr;
     val pnames =
       if length descr = 1 then ["P"]
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
@@ -47,7 +47,7 @@
     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 (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+          val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
           val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
           val recs = filter (Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
           val frees = tnames ~~ Ts;
@@ -128,7 +128,7 @@
         (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
       ||> Sign.restore_naming thy;
 
-    val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
+    val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr])) []);
     val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
     val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
     val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
@@ -157,8 +157,7 @@
   in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
 
 
-fun make_casedists sorts
-    ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
+fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
   let
     val cert = cterm_of thy;
     val rT = TFree ("'P", HOLogic.typeS);
@@ -166,7 +165,7 @@
 
     fun make_casedist_prem T (cname, cargs) =
       let
-        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr) 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)
@@ -178,7 +177,7 @@
       end;
 
     val SOME (_, _, constrs) = AList.lookup (op =) descr index;
-    val T = nth (Datatype_Aux.get_rec_types descr sorts) index;
+    val T = nth (Datatype_Aux.get_rec_types descr) index;
     val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
     val r = Const (case_name, map fastype_of rs ---> T --> rT);
 
@@ -233,8 +232,8 @@
       val info :: _ = infos;
     in
       thy
-      |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
-      |> fold_rev (make_casedists (#sorts info)) infos
+      |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
+      |> fold_rev make_casedists infos
     end;
 
 val setup = Datatype.interpretation add_dt_realizers;
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -56,14 +56,14 @@
 
 fun prove_size_thms (info : Datatype.info) new_type_names thy =
   let
-    val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info;
+    val {descr, rec_names, rec_rewrites, induct, ...} = info;
     val l = length new_type_names;
     val descr' = List.take (descr, l);
     val (rec_names1, rec_names2) = chop l rec_names;
-    val recTs = Datatype_Aux.get_rec_types descr sorts;
+    val recTs = Datatype_Aux.get_rec_types descr;
     val (recTs1, recTs2) = chop l recTs;
     val (_, (_, paramdts, _)) :: _ = descr;
-    val paramTs = map (Datatype_Aux.typ_of_dtyp descr sorts) paramdts;
+    val paramTs = map (Datatype_Aux.typ_of_dtyp descr) paramdts;
     val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
       map (fn T as TFree (s, _) =>
         let
@@ -94,7 +94,7 @@
     (* instantiation for primrec combinator *)
     fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
       let
-        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
         val k = length (filter Datatype_Aux.is_rec_type cargs);
         val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
           if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
@@ -172,7 +172,7 @@
     (* characteristic equations for size functions *)
     fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
       let
-        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+        val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
         val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
         val ts = map_filter (fn (sT as (s, T), dt) =>
           Option.map (fn sz => sz $ Free sT)
diff -r 08e44ea5ac69 -r ff7bdc67e8cb src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Dec 12 20:28:34 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Dec 12 23:06:41 2011 +0100
@@ -903,9 +903,9 @@
 fun datatype_names_of_case_name thy case_name =
   map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
 
-fun make_case_distribs new_type_names descr sorts thy =
+fun make_case_distribs new_type_names descr thy =
   let
-    val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
+    val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f";
     fun make comb =
       let
         val Type ("fun", [T, T']) = fastype_of comb;
@@ -932,10 +932,10 @@
 
 fun case_rewrites thy Tcon =
   let
-    val {descr, sorts, ...} = Datatype.the_info thy Tcon
+    val {descr, ...} = Datatype.the_info thy Tcon
   in
     map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
-      (make_case_distribs [Tcon] [descr] sorts thy)
+      (make_case_distribs [Tcon] [descr] thy)
   end
 
 fun instantiated_case_rewrites thy Tcon =