datatype dtyp with explicit sort information;
authorwenzelm
Mon Dec 12 23:05:21 2011 +0100 (2011-12-12)
changeset 45822843dc212f69e
parent 45821 c2f6c50e3d42
child 45825 ff7bdc67e8cb
datatype dtyp with explicit sort information;
tuned messages;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Dec 12 20:55:57 2011 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Dec 12 23:05:21 2011 +0100
     1.3 @@ -77,7 +77,6 @@
     1.4  type nominal_datatype_info =
     1.5    {index : int,
     1.6     descr : descr,
     1.7 -   sorts : (string * sort) list,
     1.8     rec_names : string list,
     1.9     rec_rewrites : thm list,
    1.10     induction : thm,
    1.11 @@ -100,12 +99,11 @@
    1.12  
    1.13  (**** make datatype info ****)
    1.14  
    1.15 -fun make_dt_info descr sorts induct reccomb_names rec_thms
    1.16 +fun make_dt_info descr induct reccomb_names rec_thms
    1.17      (i, (((_, (tname, _, _)), distinct), inject)) =
    1.18    (tname,
    1.19     {index = i,
    1.20      descr = descr,
    1.21 -    sorts = sorts,
    1.22      rec_names = reccomb_names,
    1.23      rec_rewrites = rec_thms,
    1.24      induction = induct,
    1.25 @@ -245,7 +243,7 @@
    1.26      val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
    1.27  
    1.28      val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
    1.29 -    fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
    1.30 +    fun nth_dtyp i = typ_of_dtyp descr (DtRec i);
    1.31  
    1.32      val big_name = space_implode "_" new_type_names;
    1.33  
    1.34 @@ -268,7 +266,7 @@
    1.35        let val T = nth_dtyp i
    1.36        in map (fn (cname, dts) =>
    1.37          let
    1.38 -          val Ts = map (typ_of_dtyp descr sorts) dts;
    1.39 +          val Ts = map (typ_of_dtyp descr) dts;
    1.40            val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
    1.41            val args = map Free (names ~~ Ts);
    1.42            val c = Const (cname, Ts ---> T);
    1.43 @@ -518,7 +516,7 @@
    1.44            apfst (cons dt) (strip_option dt')
    1.45        | strip_option dt = ([], dt);
    1.46  
    1.47 -    val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
    1.48 +    val dt_atomTs = distinct op = (map (typ_of_dtyp descr)
    1.49        (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
    1.50      val dt_atoms = map (fst o dest_Type) dt_atomTs;
    1.51  
    1.52 @@ -528,9 +526,9 @@
    1.53            let
    1.54              val (dts, dt') = strip_option dt;
    1.55              val (dts', dt'') = strip_dtyp dt';
    1.56 -            val Ts = map (typ_of_dtyp descr sorts) dts;
    1.57 -            val Us = map (typ_of_dtyp descr sorts) dts';
    1.58 -            val T = typ_of_dtyp descr sorts dt'';
    1.59 +            val Ts = map (typ_of_dtyp descr) dts;
    1.60 +            val Us = map (typ_of_dtyp descr) dts';
    1.61 +            val T = typ_of_dtyp descr dt'';
    1.62              val free = mk_Free "x" (Us ---> T) j;
    1.63              val free' = app_bnds free (length Us);
    1.64              fun mk_abs_fun T (i, t) =
    1.65 @@ -756,14 +754,14 @@
    1.66        map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
    1.67          (constrs ~~ idxss)))) (descr'' ~~ ndescr);
    1.68  
    1.69 -    fun nth_dtyp' i = typ_of_dtyp descr'' sorts (DtRec i);
    1.70 +    fun nth_dtyp' i = typ_of_dtyp descr'' (DtRec i);
    1.71  
    1.72      val rep_names = map (fn s =>
    1.73        Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
    1.74      val abs_names = map (fn s =>
    1.75        Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
    1.76  
    1.77 -    val recTs = get_rec_types descr'' sorts;
    1.78 +    val recTs = get_rec_types descr'';
    1.79      val newTs' = take (length new_type_names) recTs';
    1.80      val newTs = take (length new_type_names) recTs;
    1.81  
    1.82 @@ -774,17 +772,17 @@
    1.83        let
    1.84          fun constr_arg (dts, dt) (j, l_args, r_args) =
    1.85            let
    1.86 -            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
    1.87 +            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' dt) i)
    1.88                (dts ~~ (j upto j + length dts - 1))
    1.89 -            val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
    1.90 +            val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts)
    1.91            in
    1.92              (j + length dts + 1,
    1.93               xs @ x :: l_args,
    1.94               fold_rev mk_abs_fun xs
    1.95                 (case dt of
    1.96                    DtRec k => if k < length new_type_names then
    1.97 -                      Const (nth rep_names k, typ_of_dtyp descr'' sorts dt -->
    1.98 -                        typ_of_dtyp descr sorts dt) $ x
    1.99 +                      Const (nth rep_names k, typ_of_dtyp descr'' dt -->
   1.100 +                        typ_of_dtyp descr dt) $ x
   1.101                      else error "nested recursion not (yet) supported"
   1.102                  | _ => x) :: r_args)
   1.103            end
   1.104 @@ -866,7 +864,7 @@
   1.105  
   1.106      (* prove distinctness theorems *)
   1.107  
   1.108 -    val distinct_props = Datatype_Prop.make_distincts descr' sorts;
   1.109 +    val distinct_props = Datatype_Prop.make_distincts descr';
   1.110      val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
   1.111        dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
   1.112          constr_rep_thmss dist_lemmas;
   1.113 @@ -902,10 +900,10 @@
   1.114  
   1.115            fun constr_arg (dts, dt) (j, l_args, r_args) =
   1.116              let
   1.117 -              val Ts = map (typ_of_dtyp descr'' sorts) dts;
   1.118 +              val Ts = map (typ_of_dtyp descr'') dts;
   1.119                val xs = map (fn (T, i) => mk_Free "x" T i)
   1.120                  (Ts ~~ (j upto j + length dts - 1))
   1.121 -              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.122 +              val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts)
   1.123              in
   1.124                (j + length dts + 1,
   1.125                 xs @ x :: l_args,
   1.126 @@ -952,11 +950,11 @@
   1.127  
   1.128            fun make_inj (dts, dt) (j, args1, args2, eqs) =
   1.129              let
   1.130 -              val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
   1.131 +              val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
   1.132                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   1.133                val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
   1.134 -              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts);
   1.135 -              val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.136 +              val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts);
   1.137 +              val y = mk_Free "y" (typ_of_dtyp descr'' dt) (j + length dts);
   1.138              in
   1.139                (j + length dts + 1,
   1.140                 xs @ (x :: args1), ys @ (y :: args2),
   1.141 @@ -995,9 +993,9 @@
   1.142  
   1.143            fun process_constr (dts, dt) (j, args1, args2) =
   1.144              let
   1.145 -              val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
   1.146 +              val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
   1.147                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   1.148 -              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.149 +              val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts);
   1.150              in
   1.151                (j + length dts + 1,
   1.152                 xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
   1.153 @@ -1066,7 +1064,7 @@
   1.154  
   1.155      val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
   1.156  
   1.157 -    val dt_induct_prop = Datatype_Prop.make_ind descr' sorts;
   1.158 +    val dt_induct_prop = Datatype_Prop.make_ind descr';
   1.159      val dt_induct = Goal.prove_global thy8 []
   1.160        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.161        (fn {prems, ...} => EVERY
   1.162 @@ -1163,8 +1161,8 @@
   1.163      fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
   1.164        let
   1.165          val recs = filter is_rec_type cargs;
   1.166 -        val Ts = map (typ_of_dtyp descr'' sorts) cargs;
   1.167 -        val recTs' = map (typ_of_dtyp descr'' sorts) recs;
   1.168 +        val Ts = map (typ_of_dtyp descr'') cargs;
   1.169 +        val recTs' = map (typ_of_dtyp descr'') recs;
   1.170          val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
   1.171          val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   1.172          val frees = tnames ~~ Ts;
   1.173 @@ -1416,7 +1414,7 @@
   1.174  
   1.175      val used = fold Term.add_tfree_namesT recTs [];
   1.176  
   1.177 -    val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
   1.178 +    val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' used;
   1.179  
   1.180      val rec_sort = if null dt_atomTs then HOLogic.typeS else
   1.181        Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
   1.182 @@ -1459,7 +1457,7 @@
   1.183      fun make_rec_intr T p rec_set ((cname, cargs), idxs)
   1.184          (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) =
   1.185        let
   1.186 -        val Ts = map (typ_of_dtyp descr'' sorts) cargs;
   1.187 +        val Ts = map (typ_of_dtyp descr'') cargs;
   1.188          val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
   1.189          val frees' = partition_cargs idxs frees;
   1.190          val binders = maps fst frees';
   1.191 @@ -2046,9 +2044,9 @@
   1.192               resolve_tac rec_intrs 1,
   1.193               REPEAT (solve (prems @ rec_total_thms) prems 1)])
   1.194        end) (rec_eq_prems ~~
   1.195 -        Datatype_Prop.make_primrecs new_type_names descr' sorts thy12);
   1.196 +        Datatype_Prop.make_primrecs new_type_names descr' thy12);
   1.197  
   1.198 -    val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
   1.199 +    val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms)
   1.200        (descr1 ~~ distinct_thms ~~ inject_thms);
   1.201  
   1.202      (* FIXME: theorems are stored in database for testing only *)
     2.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Dec 12 20:55:57 2011 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Dec 12 23:05:21 2011 +0100
     2.3 @@ -61,7 +61,7 @@
     2.4  (** proof of characteristic theorems **)
     2.5  
     2.6  fun representation_proofs (config : Datatype_Aux.config) (dt_info : Datatype_Aux.info Symtab.table)
     2.7 -    descr sorts types_syntax constr_syntax case_names_induct thy =
     2.8 +    descr types_syntax constr_syntax case_names_induct thy =
     2.9    let
    2.10      val descr' = flat descr;
    2.11      val new_type_names = map (Binding.name_of o fst) types_syntax;
    2.12 @@ -74,17 +74,16 @@
    2.13      val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
    2.14  
    2.15      val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr);
    2.16 -    val leafTs' = Datatype_Aux.get_nonrec_types descr' sorts;
    2.17 -    val branchTs = Datatype_Aux.get_branching_types descr' sorts;
    2.18 +    val leafTs' = Datatype_Aux.get_nonrec_types descr';
    2.19 +    val branchTs = Datatype_Aux.get_branching_types descr';
    2.20      val branchT =
    2.21        if null branchTs then HOLogic.unitT
    2.22        else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
    2.23      val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
    2.24      val unneeded_vars =
    2.25 -      subtract (op =) (fold Term.add_tfree_namesT (leafTs' @ branchTs) []) (hd tyvars);
    2.26 -    val leafTs =
    2.27 -      leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
    2.28 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    2.29 +      subtract (op =) (fold Term.add_tfreesT (leafTs' @ branchTs) []) (hd tyvars);
    2.30 +    val leafTs = leafTs' @ map TFree unneeded_vars;
    2.31 +    val recTs = Datatype_Aux.get_rec_types descr';
    2.32      val (newTs, oldTs) = chop (length (hd descr)) recTs;
    2.33      val sumT =
    2.34        if null leafTs then HOLogic.unitT
    2.35 @@ -156,7 +155,7 @@
    2.36            (case Datatype_Aux.strip_dtyp dt of
    2.37              (dts, Datatype_Aux.DtRec k) =>
    2.38                let
    2.39 -                val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) dts;
    2.40 +                val Ts = map (Datatype_Aux.typ_of_dtyp descr') dts;
    2.41                  val free_t =
    2.42                    Datatype_Aux.app_bnds (Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
    2.43                in
    2.44 @@ -166,7 +165,7 @@
    2.45                  mk_lim free_t Ts :: ts)
    2.46                end
    2.47            | _ =>
    2.48 -              let val T = Datatype_Aux.typ_of_dtyp descr' sorts dt
    2.49 +              let val T = Datatype_Aux.typ_of_dtyp descr' dt
    2.50                in (j + 1, prems, (Leaf $ mk_inj T (Datatype_Aux.mk_Free "x" T j)) :: ts) end);
    2.51  
    2.52          val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
    2.53 @@ -194,8 +193,7 @@
    2.54        |> Sign.parent_path
    2.55        |> fold_map
    2.56          (fn (((name, mx), tvs), c) =>
    2.57 -          Typedef.add_typedef_global false NONE
    2.58 -            (name, map (rpair dummyS) tvs, mx)
    2.59 +          Typedef.add_typedef_global false NONE (name, tvs, mx)
    2.60              (Collect $ Const (c, UnivT')) NONE
    2.61              (rtac exI 1 THEN rtac CollectI 1 THEN
    2.62                QUIET_BREADTH_FIRST (has_fewer_prems 1)
    2.63 @@ -223,7 +221,7 @@
    2.64        let
    2.65          fun constr_arg dt (j, l_args, r_args) =
    2.66            let
    2.67 -            val T = Datatype_Aux.typ_of_dtyp descr' sorts dt;
    2.68 +            val T = Datatype_Aux.typ_of_dtyp descr' dt;
    2.69              val free_t = Datatype_Aux.mk_Free "x" T j;
    2.70            in
    2.71              (case (Datatype_Aux.strip_dtyp dt, strip_type T) of
    2.72 @@ -235,7 +233,7 @@
    2.73            end;
    2.74  
    2.75          val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
    2.76 -        val constrT = (map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs) ---> T;
    2.77 +        val constrT = map (Datatype_Aux.typ_of_dtyp descr') cargs ---> T;
    2.78          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    2.79          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    2.80          val lhs = list_comb (Const (cname, constrT), l_args);
    2.81 @@ -305,7 +303,7 @@
    2.82  
    2.83      fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
    2.84        let
    2.85 -        val argTs = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
    2.86 +        val argTs = map (Datatype_Aux.typ_of_dtyp descr') cargs;
    2.87          val T = nth recTs k;
    2.88          val rep_name = nth all_rep_names k;
    2.89          val rep_const = Const (rep_name, T --> Univ_elT);
    2.90 @@ -313,7 +311,7 @@
    2.91  
    2.92          fun process_arg ks' dt (i2, i2', ts, Ts) =
    2.93            let
    2.94 -            val T' = Datatype_Aux.typ_of_dtyp descr' sorts dt;
    2.95 +            val T' = Datatype_Aux.typ_of_dtyp descr' dt;
    2.96              val (Us, U) = strip_type T'
    2.97            in
    2.98              (case Datatype_Aux.strip_dtyp dt of
    2.99 @@ -556,7 +554,7 @@
   2.100        in prove ts end;
   2.101  
   2.102      val distinct_thms =
   2.103 -      map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr sorts);
   2.104 +      map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr);
   2.105  
   2.106      (* prove injectivity of constructors *)
   2.107  
   2.108 @@ -582,7 +580,7 @@
   2.109  
   2.110      val constr_inject =
   2.111        map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   2.112 -        ((Datatype_Prop.make_injs descr sorts) ~~ constr_rep_thms);
   2.113 +        (Datatype_Prop.make_injs descr ~~ constr_rep_thms);
   2.114  
   2.115      val ((constr_inject', distinct_thms'), thy6) =
   2.116        thy5
   2.117 @@ -642,7 +640,7 @@
   2.118        else map (Free o apfst fst o dest_Var) Ps;
   2.119      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
   2.120  
   2.121 -    val dt_induct_prop = Datatype_Prop.make_ind descr sorts;
   2.122 +    val dt_induct_prop = Datatype_Prop.make_ind descr;
   2.123      val dt_induct =
   2.124        Skip_Proof.prove_global thy6 []
   2.125        (Logic.strip_imp_prems dt_induct_prop)
   2.126 @@ -698,7 +696,7 @@
   2.127      val _ =
   2.128        (case duplicates (op =) (map fst new_dts) of
   2.129          [] => ()
   2.130 -      | dups => error ("Duplicate datatypes: " ^ commas dups));
   2.131 +      | dups => error ("Duplicate datatypes: " ^ commas_quote dups));
   2.132  
   2.133      fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
   2.134        let
   2.135 @@ -721,21 +719,28 @@
   2.136        in
   2.137          (case duplicates (op =) (map fst constrs') of
   2.138            [] =>
   2.139 -            (dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
   2.140 +            (dts' @ [(i, (Sign.full_name tmp_thy tname, tvs, constrs'))],
   2.141                constr_syntax @ [constr_syntax'], sorts', i + 1)
   2.142          | dups =>
   2.143 -            error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname))
   2.144 +            error ("Duplicate constructors " ^ commas_quote dups ^
   2.145 +              " in datatype " ^ Binding.print tname))
   2.146        end;
   2.147  
   2.148 -    val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
   2.149 -    val sorts =
   2.150 -      sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
   2.151 +    val (dts0, constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
   2.152 +    val tmp_ctxt' = tmp_ctxt |> fold (Variable.declare_typ o TFree) sorts';
   2.153 +
   2.154 +    val dts' = dts0 |> map (fn (i, (name, tvs, cs)) =>
   2.155 +      let
   2.156 +        val args = tvs |>
   2.157 +          map (fn a => Datatype_Aux.DtTFree (a, Proof_Context.default_sort tmp_ctxt' (a, ~1)));
   2.158 +      in (i, (name, args, cs)) end);
   2.159 +
   2.160      val dt_info = Datatype_Data.get_all thy;
   2.161 -    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' sorts dt_info dts' i;
   2.162 +    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' dt_info dts' i;
   2.163      val _ =
   2.164        Datatype_Aux.check_nonempty descr
   2.165          handle (exn as Datatype_Aux.Datatype_Empty s) =>
   2.166 -          if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   2.167 +          if #strict config then error ("Nonemptiness check failed for datatype " ^ quote s)
   2.168            else reraise exn;
   2.169  
   2.170      val _ =
   2.171 @@ -743,10 +748,10 @@
   2.172          ("Constructing datatype(s) " ^ commas_quote (map (Binding.name_of o #2) dts));
   2.173    in
   2.174      thy
   2.175 -    |> representation_proofs config dt_info descr sorts types_syntax constr_syntax
   2.176 +    |> representation_proofs config dt_info descr types_syntax constr_syntax
   2.177        (Datatype_Data.mk_case_names_induct (flat descr))
   2.178      |-> (fn (inject, distinct, induct) =>
   2.179 -      Datatype_Data.derive_datatype_props config dt_names descr sorts induct inject distinct)
   2.180 +      Datatype_Data.derive_datatype_props config dt_names descr induct inject distinct)
   2.181    end;
   2.182  
   2.183  val add_datatype = gen_add_datatype Datatype_Data.cert_typ;
     3.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Dec 12 20:55:57 2011 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Dec 12 23:05:21 2011 +0100
     3.3 @@ -9,27 +9,21 @@
     3.4  signature DATATYPE_ABS_PROOFS =
     3.5  sig
     3.6    include DATATYPE_COMMON
     3.7 -  val prove_casedist_thms : config -> string list ->
     3.8 -    descr list -> (string * sort) list -> thm ->
     3.9 +  val prove_casedist_thms : config -> string list -> descr list -> thm ->
    3.10      attribute list -> theory -> thm list * theory
    3.11 -  val prove_primrec_thms : config -> string list ->
    3.12 -    descr list -> (string * sort) list ->
    3.13 -      (string -> thm list) -> thm list list -> thm list list * thm list list ->
    3.14 -        thm -> theory -> (string list * thm list) * theory
    3.15 -  val prove_case_thms : config -> string list ->
    3.16 -    descr list -> (string * sort) list ->
    3.17 -      string list -> thm list -> theory -> (thm list list * string list) * theory
    3.18 -  val prove_split_thms : config -> string list ->
    3.19 -    descr list -> (string * sort) list ->
    3.20 -      thm list list -> thm list list -> thm list -> thm list list -> theory ->
    3.21 -        (thm * thm) list * theory
    3.22 +  val prove_primrec_thms : config -> string list -> descr list ->
    3.23 +    (string -> thm list) -> thm list list -> thm list list * thm list list ->
    3.24 +      thm -> theory -> (string list * thm list) * theory
    3.25 +  val prove_case_thms : config -> string list -> descr list ->
    3.26 +    string list -> thm list -> theory -> (thm list list * string list) * theory
    3.27 +  val prove_split_thms : config -> string list -> descr list ->
    3.28 +    thm list list -> thm list list -> thm list -> thm list list -> theory ->
    3.29 +    (thm * thm) list * theory
    3.30    val prove_nchotomys : config -> string list -> descr list ->
    3.31 -    (string * sort) list -> thm list -> theory -> thm list * theory
    3.32 -  val prove_weak_case_congs : string list -> descr list ->
    3.33 -    (string * sort) list -> theory -> thm list * theory
    3.34 -  val prove_case_congs : string list ->
    3.35 -    descr list -> (string * sort) list ->
    3.36 -      thm list -> thm list list -> theory -> thm list * theory
    3.37 +    thm list -> theory -> thm list * theory
    3.38 +  val prove_weak_case_congs : string list -> descr list -> theory -> thm list * theory
    3.39 +  val prove_case_congs : string list -> descr list ->
    3.40 +    thm list -> thm list list -> theory -> thm list * theory
    3.41  end;
    3.42  
    3.43  structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
    3.44 @@ -38,12 +32,12 @@
    3.45  (************************ case distinction theorems ***************************)
    3.46  
    3.47  fun prove_casedist_thms (config : Datatype_Aux.config)
    3.48 -    new_type_names descr sorts induct case_names_exhausts thy =
    3.49 +    new_type_names descr induct case_names_exhausts thy =
    3.50    let
    3.51      val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
    3.52  
    3.53      val descr' = flat descr;
    3.54 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    3.55 +    val recTs = Datatype_Aux.get_rec_types descr';
    3.56      val newTs = take (length (hd descr)) recTs;
    3.57  
    3.58      val maxidx = Thm.maxidx_of induct;
    3.59 @@ -75,7 +69,7 @@
    3.60        end;
    3.61  
    3.62      val casedist_thms =
    3.63 -      map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr sorts);
    3.64 +      map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr);
    3.65    in
    3.66      thy
    3.67      |> Datatype_Aux.store_thms_atts "exhaust" new_type_names
    3.68 @@ -85,7 +79,7 @@
    3.69  
    3.70  (*************************** primrec combinators ******************************)
    3.71  
    3.72 -fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr sorts
    3.73 +fun prove_primrec_thms (config : Datatype_Aux.config) new_type_names descr
    3.74      injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
    3.75    let
    3.76      val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
    3.77 @@ -94,7 +88,7 @@
    3.78      val thy0 = Sign.add_path big_name thy;
    3.79  
    3.80      val descr' = flat descr;
    3.81 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    3.82 +    val recTs = Datatype_Aux.get_rec_types descr';
    3.83      val used = fold Term.add_tfree_namesT recTs [];
    3.84      val newTs = take (length (hd descr)) recTs;
    3.85  
    3.86 @@ -106,7 +100,7 @@
    3.87        else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto length descr');
    3.88      val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
    3.89  
    3.90 -    val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr sorts used;
    3.91 +    val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr used;
    3.92  
    3.93      val rec_set_Ts =
    3.94        map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
    3.95 @@ -139,7 +133,7 @@
    3.96              | _ => (j + 1, k, prems, free1 :: t1s, t2s))
    3.97            end;
    3.98  
    3.99 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   3.100 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   3.101          val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], []);
   3.102  
   3.103        in
   3.104 @@ -268,7 +262,7 @@
   3.105               resolve_tac rec_unique_thms 1,
   3.106               resolve_tac rec_intrs 1,
   3.107               REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   3.108 -      (Datatype_Prop.make_primrecs new_type_names descr sorts thy2);
   3.109 +       (Datatype_Prop.make_primrecs new_type_names descr thy2);
   3.110    in
   3.111      thy2
   3.112      |> Sign.add_path (space_implode "_" new_type_names)
   3.113 @@ -282,24 +276,24 @@
   3.114  (***************************** case combinators *******************************)
   3.115  
   3.116  fun prove_case_thms (config : Datatype_Aux.config)
   3.117 -    new_type_names descr sorts reccomb_names primrec_thms thy =
   3.118 +    new_type_names descr reccomb_names primrec_thms thy =
   3.119    let
   3.120      val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
   3.121  
   3.122      val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
   3.123  
   3.124      val descr' = flat descr;
   3.125 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   3.126 +    val recTs = Datatype_Aux.get_rec_types descr';
   3.127      val used = fold Term.add_tfree_namesT recTs [];
   3.128      val newTs = take (length (hd descr)) recTs;
   3.129      val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
   3.130  
   3.131 -    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
   3.132 +    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
   3.133  
   3.134      val case_dummy_fns =
   3.135        map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   3.136          let
   3.137 -          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   3.138 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   3.139            val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
   3.140          in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
   3.141  
   3.142 @@ -312,7 +306,7 @@
   3.143            let
   3.144              val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
   3.145                let
   3.146 -                val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   3.147 +                val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   3.148                  val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
   3.149                  val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
   3.150                  val frees = take (length cargs) frees';
   3.151 @@ -344,7 +338,7 @@
   3.152            Skip_Proof.prove_global thy2 [] [] t
   3.153              (fn _ =>
   3.154                EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
   3.155 -        (Datatype_Prop.make_cases new_type_names descr sorts thy2);
   3.156 +        (Datatype_Prop.make_cases new_type_names descr thy2);
   3.157    in
   3.158      thy2
   3.159      |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
   3.160 @@ -357,12 +351,12 @@
   3.161  (******************************* case splitting *******************************)
   3.162  
   3.163  fun prove_split_thms (config : Datatype_Aux.config)
   3.164 -    new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy =
   3.165 +    new_type_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
   3.166    let
   3.167      val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
   3.168  
   3.169      val descr' = flat descr;
   3.170 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   3.171 +    val recTs = Datatype_Aux.get_rec_types descr';
   3.172      val newTs = take (length (hd descr)) recTs;
   3.173  
   3.174      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
   3.175 @@ -380,7 +374,7 @@
   3.176  
   3.177      val split_thm_pairs =
   3.178        map prove_split_thms
   3.179 -        ((Datatype_Prop.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
   3.180 +        (Datatype_Prop.make_splits new_type_names descr thy ~~ constr_inject ~~
   3.181            dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
   3.182  
   3.183      val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
   3.184 @@ -392,21 +386,20 @@
   3.185      |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   3.186    end;
   3.187  
   3.188 -fun prove_weak_case_congs new_type_names descr sorts thy =
   3.189 +fun prove_weak_case_congs new_type_names descr thy =
   3.190    let
   3.191      fun prove_weak_case_cong t =
   3.192       Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   3.193         (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1]);
   3.194  
   3.195      val weak_case_congs =
   3.196 -      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr sorts thy);
   3.197 +      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr thy);
   3.198  
   3.199    in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
   3.200  
   3.201  (************************* additional theorems for TFL ************************)
   3.202  
   3.203 -fun prove_nchotomys (config : Datatype_Aux.config)
   3.204 -    new_type_names descr sorts casedist_thms thy =
   3.205 +fun prove_nchotomys (config : Datatype_Aux.config) new_type_names descr casedist_thms thy =
   3.206    let
   3.207      val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
   3.208  
   3.209 @@ -424,11 +417,11 @@
   3.210        end;
   3.211  
   3.212      val nchotomys =
   3.213 -      map prove_nchotomy (Datatype_Prop.make_nchotomys descr sorts ~~ casedist_thms);
   3.214 +      map prove_nchotomy (Datatype_Prop.make_nchotomys descr ~~ casedist_thms);
   3.215  
   3.216    in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
   3.217  
   3.218 -fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
   3.219 +fun prove_case_congs new_type_names descr nchotomys case_thms thy =
   3.220    let
   3.221      fun prove_case_cong ((t, nchotomy), case_rewrites) =
   3.222        let
   3.223 @@ -452,7 +445,7 @@
   3.224  
   3.225      val case_congs =
   3.226        map prove_case_cong (Datatype_Prop.make_case_congs
   3.227 -        new_type_names descr sorts thy ~~ nchotomys ~~ case_thms);
   3.228 +        new_type_names descr thy ~~ nchotomys ~~ case_thms);
   3.229  
   3.230    in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
   3.231  
     4.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Dec 12 20:55:57 2011 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Dec 12 23:05:21 2011 +0100
     4.3 @@ -9,14 +9,13 @@
     4.4    type config = {strict : bool, quiet : bool}
     4.5    val default_config : config
     4.6    datatype dtyp =
     4.7 -      DtTFree of string
     4.8 +      DtTFree of string * sort
     4.9      | DtType of string * dtyp list
    4.10      | DtRec of int
    4.11    type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
    4.12    type info =
    4.13     {index : int,
    4.14      descr : descr,
    4.15 -    sorts : (string * sort) list,
    4.16      inject : thm list,
    4.17      distinct : thm list,
    4.18      induct : thm,
    4.19 @@ -61,23 +60,22 @@
    4.20    val dtyp_of_typ : (string * string list) list -> typ -> dtyp
    4.21    val mk_Free : string -> typ -> int -> term
    4.22    val is_rec_type : dtyp -> bool
    4.23 -  val typ_of_dtyp : descr -> (string * sort) list -> dtyp -> typ
    4.24 -  val dest_DtTFree : dtyp -> string
    4.25 +  val typ_of_dtyp : descr -> dtyp -> typ
    4.26 +  val dest_DtTFree : dtyp -> string * sort
    4.27    val dest_DtRec : dtyp -> int
    4.28    val strip_dtyp : dtyp -> dtyp list * dtyp
    4.29    val body_index : dtyp -> int
    4.30    val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
    4.31 -  val get_nonrec_types : descr -> (string * sort) list -> typ list
    4.32 -  val get_branching_types : descr -> (string * sort) list -> typ list
    4.33 +  val get_nonrec_types : descr -> typ list
    4.34 +  val get_branching_types : descr -> typ list
    4.35    val get_arities : descr -> int list
    4.36 -  val get_rec_types : descr -> (string * sort) list -> typ list
    4.37 -  val interpret_construction : descr -> (string * sort) list
    4.38 -    -> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
    4.39 -    -> ((string * typ list) * (string * 'a list) list) list
    4.40 +  val get_rec_types : descr -> typ list
    4.41 +  val interpret_construction : descr -> (string * sort) list ->
    4.42 +    {atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a} ->
    4.43 +    ((string * typ list) * (string * 'a list) list) list
    4.44    val check_nonempty : descr list -> unit
    4.45 -  val unfold_datatypes :
    4.46 -    Proof.context -> descr -> (string * sort) list -> info Symtab.table ->
    4.47 -      descr -> int -> descr list * int
    4.48 +  val unfold_datatypes : Proof.context -> descr -> info Symtab.table ->
    4.49 +    descr -> int -> descr list * int
    4.50    val find_shortest_path : descr -> int -> (string * int) option
    4.51  end;
    4.52  
    4.53 @@ -176,7 +174,7 @@
    4.54  (********************** Internal description of datatypes *********************)
    4.55  
    4.56  datatype dtyp =
    4.57 -    DtTFree of string
    4.58 +    DtTFree of string * sort
    4.59    | DtType of string * dtyp list
    4.60    | DtRec of int;
    4.61  
    4.62 @@ -188,7 +186,6 @@
    4.63  type info =
    4.64    {index : int,
    4.65     descr : descr,
    4.66 -   sorts : (string * sort) list,
    4.67     inject : thm list,
    4.68     distinct : thm list,
    4.69     induct : thm,
    4.70 @@ -206,7 +203,7 @@
    4.71  
    4.72  fun mk_Free s T i = Free (s ^ string_of_int i, T);
    4.73  
    4.74 -fun subst_DtTFree _ substs (T as DtTFree name) = the_default T (AList.lookup (op =) substs name)
    4.75 +fun subst_DtTFree _ substs (T as DtTFree a) = the_default T (AList.lookup (op =) substs a)
    4.76    | subst_DtTFree i substs (DtType (name, ts)) = DtType (name, map (subst_DtTFree i substs) ts)
    4.77    | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
    4.78  
    4.79 @@ -239,7 +236,7 @@
    4.80        end
    4.81    | name_of_typ _ = "";
    4.82  
    4.83 -fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
    4.84 +fun dtyp_of_typ _ (TFree a) = DtTFree a
    4.85    | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
    4.86    | dtyp_of_typ new_dts (Type (tname, Ts)) =
    4.87        (case AList.lookup (op =) new_dts tname of
    4.88 @@ -247,29 +244,29 @@
    4.89        | SOME vs =>
    4.90            if map (try (fst o dest_TFree)) Ts = map SOME vs then
    4.91              DtRec (find_index (curry op = tname o fst) new_dts)
    4.92 -          else error ("Illegal occurrence of recursive type " ^ tname));
    4.93 +          else error ("Illegal occurrence of recursive type " ^ quote tname));
    4.94  
    4.95 -fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, (the o AList.lookup (op =) sorts) a)
    4.96 -  | typ_of_dtyp descr sorts (DtRec i) =
    4.97 +fun typ_of_dtyp descr (DtTFree a) = TFree a
    4.98 +  | typ_of_dtyp descr (DtRec i) =
    4.99        let val (s, ds, _) = the (AList.lookup (op =) descr i)
   4.100 -      in Type (s, map (typ_of_dtyp descr sorts) ds) end
   4.101 -  | typ_of_dtyp descr sorts (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr sorts) ds);
   4.102 +      in Type (s, map (typ_of_dtyp descr) ds) end
   4.103 +  | typ_of_dtyp descr (DtType (s, ds)) = Type (s, map (typ_of_dtyp descr) ds);
   4.104  
   4.105  (* find all non-recursive types in datatype description *)
   4.106  
   4.107 -fun get_nonrec_types descr sorts =
   4.108 -  map (typ_of_dtyp descr sorts) (fold (fn (_, (_, _, constrs)) =>
   4.109 +fun get_nonrec_types descr =
   4.110 +  map (typ_of_dtyp descr) (fold (fn (_, (_, _, constrs)) =>
   4.111      fold (fn (_, cargs) => union (op =) (filter_out is_rec_type cargs)) constrs) descr []);
   4.112  
   4.113  (* get all recursive types in datatype description *)
   4.114  
   4.115 -fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
   4.116 -  Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
   4.117 +fun get_rec_types descr = map (fn (_ , (s, ds, _)) =>
   4.118 +  Type (s, map (typ_of_dtyp descr) ds)) descr;
   4.119  
   4.120  (* get all branching types *)
   4.121  
   4.122 -fun get_branching_types descr sorts =
   4.123 -  map (typ_of_dtyp descr sorts)
   4.124 +fun get_branching_types descr =
   4.125 +  map (typ_of_dtyp descr)
   4.126      (fold
   4.127        (fn (_, (_, _, constrs)) =>
   4.128          fold (fn (_, cargs) => fold (strip_dtyp #> fst #> fold (insert op =)) cargs) constrs)
   4.129 @@ -286,19 +283,21 @@
   4.130  
   4.131  fun interpret_construction descr vs {atyp, dtyp} =
   4.132    let
   4.133 -    val typ_of_dtyp = typ_of_dtyp descr vs;
   4.134 +    val typ_of =
   4.135 +      typ_of_dtyp descr #>
   4.136 +      map_atyps (fn TFree (a, _) => TFree (a, the (AList.lookup (op =) vs a)) | T => T);
   4.137      fun interpT dT =
   4.138        (case strip_dtyp dT of
   4.139          (dTs, DtRec l) =>
   4.140            let
   4.141              val (tyco, dTs', _) = the (AList.lookup (op =) descr l);
   4.142 -            val Ts = map typ_of_dtyp dTs;
   4.143 -            val Ts' = map typ_of_dtyp dTs';
   4.144 +            val Ts = map typ_of dTs;
   4.145 +            val Ts' = map typ_of dTs';
   4.146              val is_proper = forall (can dest_TFree) Ts';
   4.147            in dtyp Ts (l, is_proper) (tyco, Ts') end
   4.148 -      | _ => atyp (typ_of_dtyp dT));
   4.149 +      | _ => atyp (typ_of dT));
   4.150      fun interpC (c, dTs) = (c, map interpT dTs);
   4.151 -    fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of_dtyp dTs), map interpC cs);
   4.152 +    fun interpD (_, (tyco, dTs, cs)) = ((tyco, map typ_of dTs), map interpC cs);
   4.153    in map interpD descr end;
   4.154  
   4.155  (* nonemptiness check for datatypes *)
   4.156 @@ -323,22 +322,23 @@
   4.157  (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
   4.158  (* need to be unfolded                                         *)
   4.159  
   4.160 -fun unfold_datatypes ctxt orig_descr sorts (dt_info : info Symtab.table) descr i =
   4.161 +fun unfold_datatypes ctxt orig_descr (dt_info : info Symtab.table) descr i =
   4.162    let
   4.163      fun typ_error T msg =
   4.164        error ("Non-admissible type expression\n" ^
   4.165 -        Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
   4.166 +        Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) T) ^ "\n" ^ msg);
   4.167  
   4.168      fun get_dt_descr T i tname dts =
   4.169        (case Symtab.lookup dt_info tname of
   4.170          NONE =>
   4.171 -          typ_error T (tname ^ " is not a datatype - can't use it in nested recursion")
   4.172 +          typ_error T (quote tname ^ " is not a datatype - can't use it in nested recursion")
   4.173        | SOME {index, descr, ...} =>
   4.174            let
   4.175              val (_, vars, _) = the (AList.lookup (op =) descr index);
   4.176              val subst = map dest_DtTFree vars ~~ dts
   4.177                handle ListPair.UnequalLengths =>
   4.178 -                typ_error T ("Type constructor " ^ tname ^ " used with wrong number of arguments");
   4.179 +                typ_error T ("Type constructor " ^ quote tname ^
   4.180 +                  " used with wrong number of arguments");
   4.181            in
   4.182              (i + index,
   4.183                map (fn (j, (tn, args, cs)) =>
   4.184 @@ -359,7 +359,7 @@
   4.185                  let
   4.186                    val (index, descr) = get_dt_descr T i tname dts;
   4.187                    val (descr', i') =
   4.188 -                    unfold_datatypes ctxt orig_descr sorts dt_info descr (i + length descr);
   4.189 +                    unfold_datatypes ctxt orig_descr dt_info descr (i + length descr);
   4.190                  in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
   4.191              | _ => (i, Ts @ [T], descrs))
   4.192          end
     5.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Mon Dec 12 20:55:57 2011 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Mon Dec 12 23:05:21 2011 +0100
     5.3 @@ -36,10 +36,10 @@
     5.4  
     5.5  fun ty_info tab sT =
     5.6    (case tab sT of
     5.7 -    SOME ({descr, case_name, index, sorts, ...} : info) =>
     5.8 +    SOME ({descr, case_name, index, ...} : info) =>
     5.9        let
    5.10          val (_, (tname, dts, constrs)) = nth descr index;
    5.11 -        val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
    5.12 +        val mk_ty = Datatype_Aux.typ_of_dtyp descr;
    5.13          val T = Type (tname, map mk_ty dts);
    5.14        in
    5.15          SOME {case_name = case_name,
     6.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Dec 12 20:55:57 2011 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Dec 12 23:05:21 2011 +0100
     6.3 @@ -76,11 +76,11 @@
     6.4            | _ => NONE) cos;
     6.5      fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
     6.6        trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
     6.7 -    val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
     6.8 +    val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index);
     6.9      fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
    6.10        [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
    6.11      val distincts =
    6.12 -      maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
    6.13 +      maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index));
    6.14      val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
    6.15      val simpset =
    6.16        Simplifier.global_context thy
     7.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Dec 12 20:55:57 2011 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Dec 12 23:05:21 2011 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  signature DATATYPE_DATA =
     7.5  sig
     7.6    include DATATYPE_COMMON
     7.7 -  val derive_datatype_props : config -> string list -> descr list -> (string * sort) list ->
     7.8 +  val derive_datatype_props : config -> string list -> descr list ->
     7.9      thm -> thm list list -> thm list list -> theory -> string list * theory
    7.10    val rep_datatype : config -> (string list -> Proof.context -> Proof.context) ->
    7.11      term list -> theory -> Proof.state
    7.12 @@ -109,22 +109,19 @@
    7.13  
    7.14  fun the_spec thy dtco =
    7.15    let
    7.16 -    val {descr, index, sorts = raw_sorts, ...} = the_info thy dtco;
    7.17 +    val {descr, index, ...} = the_info thy dtco;
    7.18      val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index);
    7.19 -    val sorts =
    7.20 -      map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v)) o Datatype_Aux.dest_DtTFree) dtys;
    7.21 -    val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos;
    7.22 -  in (sorts, cos) end;
    7.23 +    val args = map Datatype_Aux.dest_DtTFree dtys;
    7.24 +    val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos;
    7.25 +  in (args, cos) end;
    7.26  
    7.27  fun the_descr thy (raw_tycos as raw_tyco :: _) =
    7.28    let
    7.29      val info = the_info thy raw_tyco;
    7.30      val descr = #descr info;
    7.31  
    7.32 -    val SOME (_, dtys, _) = AList.lookup (op =) descr (#index info);
    7.33 -    val vs =
    7.34 -      map ((fn v => (v, the (AList.lookup (op =) (#sorts info) v))) o Datatype_Aux.dest_DtTFree)
    7.35 -        dtys;
    7.36 +    val (_, dtys, _) = the (AList.lookup (op =) descr (#index info));
    7.37 +    val vs = map Datatype_Aux.dest_DtTFree dtys;
    7.38  
    7.39      fun is_DtTFree (Datatype_Aux.DtTFree _) = true
    7.40        | is_DtTFree _ = false;
    7.41 @@ -132,7 +129,7 @@
    7.42      val protoTs as (dataTs, _) =
    7.43        chop k descr
    7.44        |> (pairself o map)
    7.45 -        (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr vs) dTs));
    7.46 +        (fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr) dTs));
    7.47  
    7.48      val tycos = map fst dataTs;
    7.49      val _ =
    7.50 @@ -160,12 +157,12 @@
    7.51  
    7.52  fun get_constrs thy dtco =
    7.53    (case try (the_spec thy) dtco of
    7.54 -    SOME (sorts, cos) =>
    7.55 +    SOME (args, cos) =>
    7.56        let
    7.57          fun subst (v, sort) = TVar ((v, 0), sort);
    7.58          fun subst_ty (TFree v) = subst v
    7.59            | subst_ty ty = ty;
    7.60 -        val dty = Type (dtco, map subst sorts);
    7.61 +        val dty = Type (dtco, map subst args);
    7.62          fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
    7.63        in SOME (map mk_co cos) end
    7.64    | NONE => NONE);
    7.65 @@ -283,14 +280,13 @@
    7.66  );
    7.67  fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
    7.68  
    7.69 -fun make_dt_info descr sorts induct inducts rec_names rec_rewrites
    7.70 +fun make_dt_info descr induct inducts rec_names rec_rewrites
    7.71      (index, (((((((((((_, (tname, _, _))), inject), distinct),
    7.72        exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
    7.73          (split, split_asm))) =
    7.74    (tname,
    7.75     {index = index,
    7.76      descr = descr,
    7.77 -    sorts = sorts,
    7.78      inject = inject,
    7.79      distinct = distinct,
    7.80      induct = induct,
    7.81 @@ -306,8 +302,7 @@
    7.82      split = split,
    7.83      split_asm = split_asm});
    7.84  
    7.85 -fun derive_datatype_props config dt_names descr sorts
    7.86 -    induct inject distinct thy1 =
    7.87 +fun derive_datatype_props config dt_names descr induct inject distinct thy1 =
    7.88    let
    7.89      val thy2 = thy1 |> Theory.checkpoint;
    7.90      val flat_descr = flat descr;
    7.91 @@ -316,32 +311,28 @@
    7.92        Datatype_Aux.message config
    7.93          ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
    7.94  
    7.95 -    val (exhaust, thy3) =
    7.96 -      Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
    7.97 -        descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
    7.98 -    val (nchotomys, thy4) =
    7.99 -      Datatype_Abs_Proofs.prove_nchotomys config new_type_names
   7.100 -        descr sorts exhaust thy3;
   7.101 -    val ((rec_names, rec_rewrites), thy5) =
   7.102 -      Datatype_Abs_Proofs.prove_primrec_thms
   7.103 -        config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
   7.104 -        inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr sorts))
   7.105 -        induct thy4;
   7.106 -    val ((case_rewrites, case_names), thy6) =
   7.107 -      Datatype_Abs_Proofs.prove_case_thms
   7.108 -        config new_type_names descr sorts rec_names rec_rewrites thy5;
   7.109 -    val (case_congs, thy7) =
   7.110 -      Datatype_Abs_Proofs.prove_case_congs new_type_names
   7.111 -        descr sorts nchotomys case_rewrites thy6;
   7.112 -    val (weak_case_congs, thy8) =
   7.113 -      Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr sorts thy7;
   7.114 -    val (splits, thy9) =
   7.115 -      Datatype_Abs_Proofs.prove_split_thms
   7.116 -        config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
   7.117 +    val (exhaust, thy3) = thy2
   7.118 +      |> Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
   7.119 +        descr induct (mk_case_names_exhausts flat_descr dt_names);
   7.120 +    val (nchotomys, thy4) = thy3
   7.121 +      |> Datatype_Abs_Proofs.prove_nchotomys config new_type_names descr exhaust;
   7.122 +    val ((rec_names, rec_rewrites), thy5) = thy4
   7.123 +      |> Datatype_Abs_Proofs.prove_primrec_thms
   7.124 +        config new_type_names descr (#inject o the o Symtab.lookup (get_all thy4))
   7.125 +        inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr)) induct;
   7.126 +    val ((case_rewrites, case_names), thy6) = thy5
   7.127 +      |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites;
   7.128 +    val (case_congs, thy7) = thy6
   7.129 +      |> Datatype_Abs_Proofs.prove_case_congs new_type_names descr nchotomys case_rewrites;
   7.130 +    val (weak_case_congs, thy8) = thy7
   7.131 +      |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr;
   7.132 +    val (splits, thy9) = thy8
   7.133 +      |> Datatype_Abs_Proofs.prove_split_thms
   7.134 +        config new_type_names descr inject distinct exhaust case_rewrites;
   7.135  
   7.136      val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
   7.137      val dt_infos = map_index
   7.138 -      (make_dt_info flat_descr sorts induct inducts rec_names rec_rewrites)
   7.139 +      (make_dt_info flat_descr induct inducts rec_names rec_rewrites)
   7.140        (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
   7.141          case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
   7.142      val dt_names = map fst dt_infos;
   7.143 @@ -378,7 +369,7 @@
   7.144  
   7.145  (** declare existing type as datatype **)
   7.146  
   7.147 -fun prove_rep_datatype config dt_names descr sorts raw_inject half_distinct raw_induct thy1 =
   7.148 +fun prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct thy1 =
   7.149    let
   7.150      val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
   7.151      val new_type_names = map Long_Name.base_name dt_names;
   7.152 @@ -392,7 +383,7 @@
   7.153            [mk_case_names_induct descr])];
   7.154    in
   7.155      thy2
   7.156 -    |> derive_datatype_props config dt_names [descr] sorts induct inject distinct
   7.157 +    |> derive_datatype_props config dt_names [descr] induct inject distinct
   7.158   end;
   7.159  
   7.160  fun gen_rep_datatype prep_term config after_qed raw_ts thy =
   7.161 @@ -441,13 +432,11 @@
   7.162      val dt_names = map fst cs;
   7.163  
   7.164      fun mk_spec (i, (tyco, constr)) =
   7.165 -      (i, (tyco,
   7.166 -        map (Datatype_Aux.DtTFree o fst) vs,
   7.167 -        (map o apsnd) dtyps_of_typ constr));
   7.168 +      (i, (tyco, map Datatype_Aux.DtTFree vs, (map o apsnd) dtyps_of_typ constr));
   7.169      val descr = map_index mk_spec cs;
   7.170 -    val injs = Datatype_Prop.make_injs [descr] vs;
   7.171 -    val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs);
   7.172 -    val ind = Datatype_Prop.make_ind [descr] vs;
   7.173 +    val injs = Datatype_Prop.make_injs [descr];
   7.174 +    val half_distincts = map snd (Datatype_Prop.make_distincts [descr]);
   7.175 +    val ind = Datatype_Prop.make_ind [descr];
   7.176      val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
   7.177  
   7.178      fun after_qed' raw_thms =
   7.179 @@ -457,7 +446,7 @@
   7.180              (*FIXME somehow dubious*)
   7.181        in
   7.182          Proof_Context.background_theory_result  (* FIXME !? *)
   7.183 -          (prove_rep_datatype config dt_names descr vs raw_inject half_distinct raw_induct)
   7.184 +          (prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct)
   7.185          #-> after_qed
   7.186        end;
   7.187    in
     8.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Dec 12 20:55:57 2011 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Dec 12 23:05:21 2011 +0100
     8.3 @@ -9,27 +9,18 @@
     8.4    include DATATYPE_COMMON
     8.5    val indexify_names: string list -> string list
     8.6    val make_tnames: typ list -> string list
     8.7 -  val make_injs : descr list -> (string * sort) list -> term list list
     8.8 -  val make_distincts : descr list ->
     8.9 -    (string * sort) list -> (int * term list) list (*no symmetric inequalities*)
    8.10 -  val make_ind : descr list -> (string * sort) list -> term
    8.11 -  val make_casedists : descr list -> (string * sort) list -> term list
    8.12 -  val make_primrec_Ts : descr list -> (string * sort) list ->
    8.13 -    string list -> typ list * typ list
    8.14 -  val make_primrecs : string list -> descr list ->
    8.15 -    (string * sort) list -> theory -> term list
    8.16 -  val make_cases : string list -> descr list ->
    8.17 -    (string * sort) list -> theory -> term list list
    8.18 -  val make_splits : string list -> descr list ->
    8.19 -    (string * sort) list -> theory -> (term * term) list
    8.20 -  val make_case_combs : string list -> descr list ->
    8.21 -    (string * sort) list -> theory -> string -> term list
    8.22 -  val make_weak_case_congs : string list -> descr list ->
    8.23 -    (string * sort) list -> theory -> term list
    8.24 -  val make_case_congs : string list -> descr list ->
    8.25 -    (string * sort) list -> theory -> term list
    8.26 -  val make_nchotomys : descr list ->
    8.27 -    (string * sort) list -> term list
    8.28 +  val make_injs : descr list -> term list list
    8.29 +  val make_distincts : descr list -> (int * term list) list (*no symmetric inequalities*)
    8.30 +  val make_ind : descr list -> term
    8.31 +  val make_casedists : descr list -> term list
    8.32 +  val make_primrec_Ts : descr list -> string list -> typ list * typ list
    8.33 +  val make_primrecs : string list -> descr list -> theory -> term list
    8.34 +  val make_cases : string list -> descr list -> theory -> term list list
    8.35 +  val make_splits : string list -> descr list -> theory -> (term * term) list
    8.36 +  val make_case_combs : string list -> descr list -> theory -> string -> term list
    8.37 +  val make_weak_case_congs : string list -> descr list -> theory -> term list
    8.38 +  val make_case_congs : string list -> descr list -> theory -> term list
    8.39 +  val make_nchotomys : descr list -> term list
    8.40  end;
    8.41  
    8.42  structure Datatype_Prop : DATATYPE_PROP =
    8.43 @@ -58,14 +49,14 @@
    8.44  
    8.45  (************************* injectivity of constructors ************************)
    8.46  
    8.47 -fun make_injs descr sorts =
    8.48 +fun make_injs descr =
    8.49    let
    8.50      val descr' = flat descr;
    8.51      fun make_inj T (cname, cargs) =
    8.52        if null cargs then I
    8.53        else
    8.54          let
    8.55 -          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
    8.56 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
    8.57            val constr_t = Const (cname, Ts ---> T);
    8.58            val tnames = make_tnames Ts;
    8.59            val frees = map Free (tnames ~~ Ts);
    8.60 @@ -78,20 +69,19 @@
    8.61          end;
    8.62    in
    8.63      map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
    8.64 -      (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
    8.65 +      (hd descr) (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
    8.66    end;
    8.67  
    8.68  
    8.69  (************************* distinctness of constructors ***********************)
    8.70  
    8.71 -fun make_distincts descr sorts =
    8.72 +fun make_distincts descr =
    8.73    let
    8.74      val descr' = flat descr;
    8.75 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    8.76 +    val recTs = Datatype_Aux.get_rec_types descr';
    8.77      val newTs = take (length (hd descr)) recTs;
    8.78  
    8.79 -    fun prep_constr (cname, cargs) =
    8.80 -      (cname, map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs);
    8.81 +    fun prep_constr (cname, cargs) = (cname, map (Datatype_Aux.typ_of_dtyp descr') cargs);
    8.82  
    8.83      fun make_distincts' _ [] = []
    8.84        | make_distincts' T ((cname, cargs) :: constrs) =
    8.85 @@ -115,10 +105,10 @@
    8.86  
    8.87  (********************************* induction **********************************)
    8.88  
    8.89 -fun make_ind descr sorts =
    8.90 +fun make_ind descr =
    8.91    let
    8.92      val descr' = flat descr;
    8.93 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
    8.94 +    val recTs = Datatype_Aux.get_rec_types descr';
    8.95      val pnames =
    8.96        if length descr' = 1 then ["P"]
    8.97        else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
    8.98 @@ -139,8 +129,8 @@
    8.99            end;
   8.100  
   8.101          val recs = filter Datatype_Aux.is_rec_type cargs;
   8.102 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   8.103 -        val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
   8.104 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   8.105 +        val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
   8.106          val tnames = Name.variant_list pnames (make_tnames Ts);
   8.107          val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
   8.108          val frees = tnames ~~ Ts;
   8.109 @@ -164,13 +154,13 @@
   8.110  
   8.111  (******************************* case distinction *****************************)
   8.112  
   8.113 -fun make_casedists descr sorts =
   8.114 +fun make_casedists descr =
   8.115    let
   8.116      val descr' = flat descr;
   8.117  
   8.118      fun make_casedist_prem T (cname, cargs) =
   8.119        let
   8.120 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   8.121 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   8.122          val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
   8.123          val free_ts = map Free frees;
   8.124        in
   8.125 @@ -186,12 +176,12 @@
   8.126  
   8.127    in
   8.128      map2 make_casedist (hd descr)
   8.129 -      (take (length (hd descr)) (Datatype_Aux.get_rec_types descr' sorts))
   8.130 +      (take (length (hd descr)) (Datatype_Aux.get_rec_types descr'))
   8.131    end;
   8.132  
   8.133  (*************** characteristic equations for primrec combinator **************)
   8.134  
   8.135 -fun make_primrec_Ts descr sorts used =
   8.136 +fun make_primrec_Ts descr used =
   8.137    let
   8.138      val descr' = flat descr;
   8.139  
   8.140 @@ -203,7 +193,7 @@
   8.141      val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
   8.142        map (fn (_, cargs) =>
   8.143          let
   8.144 -          val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   8.145 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   8.146            val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
   8.147  
   8.148            fun mk_argT (dt, T) =
   8.149 @@ -214,13 +204,13 @@
   8.150  
   8.151    in (rec_result_Ts, reccomb_fn_Ts) end;
   8.152  
   8.153 -fun make_primrecs new_type_names descr sorts thy =
   8.154 +fun make_primrecs new_type_names descr thy =
   8.155    let
   8.156      val descr' = flat descr;
   8.157 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   8.158 +    val recTs = Datatype_Aux.get_rec_types descr';
   8.159      val used = fold Term.add_tfree_namesT recTs [];
   8.160  
   8.161 -    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   8.162 +    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr used;
   8.163  
   8.164      val rec_fns =
   8.165        map (uncurry (Datatype_Aux.mk_Free "f"))
   8.166 @@ -238,8 +228,8 @@
   8.167      fun make_primrec T comb_t (cname, cargs) (ts, f :: fs) =
   8.168        let
   8.169          val recs = filter Datatype_Aux.is_rec_type cargs;
   8.170 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   8.171 -        val recTs' = map (Datatype_Aux.typ_of_dtyp descr' sorts) recs;
   8.172 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   8.173 +        val recTs' = map (Datatype_Aux.typ_of_dtyp descr') recs;
   8.174          val tnames = make_tnames Ts;
   8.175          val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
   8.176          val frees = map Free (tnames ~~ Ts);
   8.177 @@ -266,17 +256,17 @@
   8.178  
   8.179  (****************** make terms of form  t_case f1 ... fn  *********************)
   8.180  
   8.181 -fun make_case_combs new_type_names descr sorts thy fname =
   8.182 +fun make_case_combs new_type_names descr thy fname =
   8.183    let
   8.184      val descr' = flat descr;
   8.185 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   8.186 +    val recTs = Datatype_Aux.get_rec_types descr';
   8.187      val used = fold Term.add_tfree_namesT recTs [];
   8.188      val newTs = take (length (hd descr)) recTs;
   8.189      val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
   8.190  
   8.191      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   8.192        map (fn (_, cargs) =>
   8.193 -        let val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs
   8.194 +        let val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs
   8.195          in Ts ---> T' end) constrs) (hd descr);
   8.196  
   8.197      val case_names = map (fn s => Sign.intern_const thy (s ^ "_case")) new_type_names;
   8.198 @@ -289,15 +279,15 @@
   8.199  
   8.200  (**************** characteristic equations for case combinator ****************)
   8.201  
   8.202 -fun make_cases new_type_names descr sorts thy =
   8.203 +fun make_cases new_type_names descr thy =
   8.204    let
   8.205      val descr' = flat descr;
   8.206 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   8.207 +    val recTs = Datatype_Aux.get_rec_types descr';
   8.208      val newTs = take (length (hd descr)) recTs;
   8.209  
   8.210      fun make_case T comb_t ((cname, cargs), f) =
   8.211        let
   8.212 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   8.213 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   8.214          val frees = map Free ((make_tnames Ts) ~~ Ts);
   8.215        in
   8.216          HOLogic.mk_Trueprop
   8.217 @@ -307,16 +297,16 @@
   8.218    in
   8.219      map (fn (((_, (_, _, constrs)), T), comb_t) =>
   8.220        map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
   8.221 -        ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
   8.222 +        ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr thy "f"))
   8.223    end;
   8.224  
   8.225  
   8.226  (*************************** the "split" - equations **************************)
   8.227  
   8.228 -fun make_splits new_type_names descr sorts thy =
   8.229 +fun make_splits new_type_names descr thy =
   8.230    let
   8.231      val descr' = flat descr;
   8.232 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   8.233 +    val recTs = Datatype_Aux.get_rec_types descr';
   8.234      val used' = fold Term.add_tfree_namesT recTs [];
   8.235      val newTs = take (length (hd descr)) recTs;
   8.236      val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
   8.237 @@ -329,7 +319,7 @@
   8.238  
   8.239          fun process_constr ((cname, cargs), f) (t1s, t2s) =
   8.240            let
   8.241 -            val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   8.242 +            val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   8.243              val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
   8.244              val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees));
   8.245              val P' = P $ list_comb (f, frees);
   8.246 @@ -348,14 +338,14 @@
   8.247        end
   8.248  
   8.249    in
   8.250 -    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr sorts thy "f")
   8.251 +    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr thy "f")
   8.252    end;
   8.253  
   8.254  (************************* additional rules for TFL ***************************)
   8.255  
   8.256 -fun make_weak_case_congs new_type_names descr sorts thy =
   8.257 +fun make_weak_case_congs new_type_names descr thy =
   8.258    let
   8.259 -    val case_combs = make_case_combs new_type_names descr sorts thy "f";
   8.260 +    val case_combs = make_case_combs new_type_names descr thy "f";
   8.261  
   8.262      fun mk_case_cong comb =
   8.263        let
   8.264 @@ -382,10 +372,10 @@
   8.265   *      (ty_case f1..fn M = ty_case g1..gn M')
   8.266   *---------------------------------------------------------------------------*)
   8.267  
   8.268 -fun make_case_congs new_type_names descr sorts thy =
   8.269 +fun make_case_congs new_type_names descr thy =
   8.270    let
   8.271 -    val case_combs = make_case_combs new_type_names descr sorts thy "f";
   8.272 -    val case_combs' = make_case_combs new_type_names descr sorts thy "g";
   8.273 +    val case_combs = make_case_combs new_type_names descr thy "f";
   8.274 +    val case_combs' = make_case_combs new_type_names descr thy "g";
   8.275  
   8.276      fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
   8.277        let
   8.278 @@ -423,15 +413,15 @@
   8.279   *    !v. (? y1..yi. v = C1 y1..yi) | ... | (? y1..yj. v = Cn y1..yj)
   8.280   *---------------------------------------------------------------------------*)
   8.281  
   8.282 -fun make_nchotomys descr sorts =
   8.283 +fun make_nchotomys descr =
   8.284    let
   8.285      val descr' = flat descr;
   8.286 -    val recTs = Datatype_Aux.get_rec_types descr' sorts;
   8.287 +    val recTs = Datatype_Aux.get_rec_types descr';
   8.288      val newTs = take (length (hd descr)) recTs;
   8.289  
   8.290      fun mk_eqn T (cname, cargs) =
   8.291        let
   8.292 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
   8.293 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   8.294          val tnames = Name.variant_list ["v"] (make_tnames Ts);
   8.295          val frees = tnames ~~ Ts;
   8.296        in
     9.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Dec 12 20:55:57 2011 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Dec 12 23:05:21 2011 +0100
     9.3 @@ -25,9 +25,9 @@
     9.4  fun tname_of (Type (s, _)) = s
     9.5    | tname_of _ = "";
     9.6  
     9.7 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
     9.8 +fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
     9.9    let
    9.10 -    val recTs = Datatype_Aux.get_rec_types descr sorts;
    9.11 +    val recTs = Datatype_Aux.get_rec_types descr;
    9.12      val pnames =
    9.13        if length descr = 1 then ["P"]
    9.14        else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
    9.15 @@ -47,7 +47,7 @@
    9.16      val (prems, rec_fns) = split_list (flat (fst (fold_map
    9.17        (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    9.18          let
    9.19 -          val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
    9.20 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
    9.21            val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
    9.22            val recs = filter (Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    9.23            val frees = tnames ~~ Ts;
    9.24 @@ -128,7 +128,7 @@
    9.25          (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
    9.26        ||> Sign.restore_naming thy;
    9.27  
    9.28 -    val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
    9.29 +    val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr])) []);
    9.30      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    9.31      val ivs1 = map Var (filter_out (fn (_, T) => @{type_name bool} = tname_of (body_type T)) ivs);
    9.32      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
    9.33 @@ -157,8 +157,7 @@
    9.34    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    9.35  
    9.36  
    9.37 -fun make_casedists sorts
    9.38 -    ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
    9.39 +fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info) thy =
    9.40    let
    9.41      val cert = cterm_of thy;
    9.42      val rT = TFree ("'P", HOLogic.typeS);
    9.43 @@ -166,7 +165,7 @@
    9.44  
    9.45      fun make_casedist_prem T (cname, cargs) =
    9.46        let
    9.47 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
    9.48 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
    9.49          val frees = Name.variant_list ["P", "y"] (Datatype_Prop.make_tnames Ts) ~~ Ts;
    9.50          val free_ts = map Free frees;
    9.51          val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
    9.52 @@ -178,7 +177,7 @@
    9.53        end;
    9.54  
    9.55      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
    9.56 -    val T = nth (Datatype_Aux.get_rec_types descr sorts) index;
    9.57 +    val T = nth (Datatype_Aux.get_rec_types descr) index;
    9.58      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
    9.59      val r = Const (case_name, map fastype_of rs ---> T --> rT);
    9.60  
    9.61 @@ -233,8 +232,8 @@
    9.62        val info :: _ = infos;
    9.63      in
    9.64        thy
    9.65 -      |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
    9.66 -      |> fold_rev (make_casedists (#sorts info)) infos
    9.67 +      |> fold_rev (make_ind info) (subsets 0 (length (#descr info) - 1))
    9.68 +      |> fold_rev make_casedists infos
    9.69      end;
    9.70  
    9.71  val setup = Datatype.interpretation add_dt_realizers;
    10.1 --- a/src/HOL/Tools/Function/size.ML	Mon Dec 12 20:55:57 2011 +0100
    10.2 +++ b/src/HOL/Tools/Function/size.ML	Mon Dec 12 23:05:21 2011 +0100
    10.3 @@ -56,14 +56,14 @@
    10.4  
    10.5  fun prove_size_thms (info : Datatype.info) new_type_names thy =
    10.6    let
    10.7 -    val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info;
    10.8 +    val {descr, rec_names, rec_rewrites, induct, ...} = info;
    10.9      val l = length new_type_names;
   10.10      val descr' = List.take (descr, l);
   10.11      val (rec_names1, rec_names2) = chop l rec_names;
   10.12 -    val recTs = Datatype_Aux.get_rec_types descr sorts;
   10.13 +    val recTs = Datatype_Aux.get_rec_types descr;
   10.14      val (recTs1, recTs2) = chop l recTs;
   10.15      val (_, (_, paramdts, _)) :: _ = descr;
   10.16 -    val paramTs = map (Datatype_Aux.typ_of_dtyp descr sorts) paramdts;
   10.17 +    val paramTs = map (Datatype_Aux.typ_of_dtyp descr) paramdts;
   10.18      val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
   10.19        map (fn T as TFree (s, _) =>
   10.20          let
   10.21 @@ -94,7 +94,7 @@
   10.22      (* instantiation for primrec combinator *)
   10.23      fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
   10.24        let
   10.25 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
   10.26 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
   10.27          val k = length (filter Datatype_Aux.is_rec_type cargs);
   10.28          val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
   10.29            if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
   10.30 @@ -172,7 +172,7 @@
   10.31      (* characteristic equations for size functions *)
   10.32      fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
   10.33        let
   10.34 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
   10.35 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
   10.36          val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
   10.37          val ts = map_filter (fn (sT as (s, T), dt) =>
   10.38            Option.map (fn sz => sz $ Free sT)
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Dec 12 20:55:57 2011 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Dec 12 23:05:21 2011 +0100
    11.3 @@ -903,9 +903,9 @@
    11.4  fun datatype_names_of_case_name thy case_name =
    11.5    map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
    11.6  
    11.7 -fun make_case_distribs new_type_names descr sorts thy =
    11.8 +fun make_case_distribs new_type_names descr thy =
    11.9    let
   11.10 -    val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
   11.11 +    val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f";
   11.12      fun make comb =
   11.13        let
   11.14          val Type ("fun", [T, T']) = fastype_of comb;
   11.15 @@ -932,10 +932,10 @@
   11.16  
   11.17  fun case_rewrites thy Tcon =
   11.18    let
   11.19 -    val {descr, sorts, ...} = Datatype.the_info thy Tcon
   11.20 +    val {descr, ...} = Datatype.the_info thy Tcon
   11.21    in
   11.22      map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
   11.23 -      (make_case_distribs [Tcon] [descr] sorts thy)
   11.24 +      (make_case_distribs [Tcon] [descr] thy)
   11.25    end
   11.26  
   11.27  fun instantiated_case_rewrites thy Tcon =