src/HOL/Nominal/nominal_datatype.ML

 type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
 
 type nominal_datatype_info =
   {index : int,
    descr : descr,
-   sorts : (string * sort) list,
    rec_names : string list,
    rec_rewrites : thm list,
    induction : thm,
    distinct : thm list,
    inject : thm list};

 val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
 
 
 (**** 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,
     distinct = distinct,
     inject = inject});

     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
 
     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;
 
 
     (**** define permutation functions ****)

 
     val perm_eqs = maps (fn (i, (_, _, constrs)) =>
       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);
           fun perm_arg (dt, x) =
             let val T = type_of x

            | _ => ([], dtf))
       | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
           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;
 
     fun make_intr s T (cname, cargs) =
       let
         fun mk_prem dt (j, j', prems, ts) =
           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) =
               let val U = fastype_of t
               in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->

 
     val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
       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;
 
     val full_new_type_names = map (Sign.full_bname thy) new_type_names;
 
     fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
         (thy, defs, eqns) =
       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
 
         val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);

 
     val perm_rep_perm_thms = maps prove_perm_rep_perm (atoms ~~ perm_closed_thmss);
 
     (* 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;
 
     fun prove_distinct_thms _ (_, []) = []

             let val T = fastype_of t
             in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
 
           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,
                map perm (xs @ [x]) @ r_args)
             end

           val cname = Sign.intern_const thy8
             (Long_Name.append tname (Long_Name.base_name cname));
 
           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),
                HOLogic.mk_eq
                  (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)

             (Long_Name.append tname (Long_Name.base_name cname));
           val atomT = Type (atom, []);
 
           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)
             end;
 

     val indrule_lemma' = cterm_instantiate
       (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
 
     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
         [rtac indrule_lemma' 1,
          (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,

           mk_fresh2 (p :: xss) yss;
 
     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;
         val frees' = partition_cargs idxs frees;
         val z = (singleton (Name.variant_list tnames) "z", fsT);

 
     val _ = warning "defining recursion combinator ...";
 
     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);
 
     val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';

     val rec_ctxt = Free ("z", fsT');
 
     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';
         val atomTs = distinct op = (maps (map snd o fst) frees');
         val recs = map_filter

              rtac the1_equality 1,
              solve rec_unique_thms prems 1,
              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);
-
-    val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
+        Datatype_Prop.make_primrecs new_type_names descr' thy12);
+
+    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 *)
     val (_, thy13) = thy12 |>
       Global_Theory.add_thmss