--- a/Nominal/Perm.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Perm.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -54,12 +54,11 @@
 *}
 
 ML {*
-(* TODO: full_name can be obtained from new_type_names with Datatype *)
-fun define_raw_perms new_type_names full_tnames thy =
+fun define_raw_perms (dt_info : info) number thy =
 let
-  val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames);
-  (* TODO: [] should be the sorts that we'll take from the specification *)
-  val sorts = [];
+  val {descr, induct, sorts, ...} = dt_info;
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
+  val full_tnames = List.take (all_full_tnames, number);
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "permute_" ^ name_of_typ (nth_dtyp i)) descr);
@@ -101,8 +100,8 @@
     val ((perm_frees, perm_ldef), lthy') =
       Primrec.add_primrec
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
-    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
-    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
+    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number);
+    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number)
     val perms_name = space_implode "_" perm_names'
     val perms_zero_bind = Binding.name (perms_name ^ "_zero")
     val perms_append_bind = Binding.name (perms_name ^ "_append")