diff -r 687369ae8f81 -r 1fe84fd8f8a4 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Fri May 21 10:47:07 2010 +0200
+++ b/Nominal/Perm.thy	Fri May 21 10:47:45 2010 +0200
@@ -7,20 +7,32 @@
 
 ML {*
 (* returns the type of the nth datatype *)
-fun nth_dtyp dt_descr sorts i = 
-  Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i);
+fun nth_dtyp descr sorts n = 
+  Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
+
+(* returns the constructors of the nth datatype *)
+fun nth_dtyp_constrs descr n = 
+let
+  val (_, (_, _, constrs)) = nth descr n
+in
+  constrs
+end
+
+(* returns the types of the constructors of the nth datatype *)
+fun nth_dtyp_constr_typs descr sorts n = 
+  map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n)
 *}
 
 ML {*
 (* generates for every datatype a name str ^ dt_name 
    plus and index for multiple occurences of a string *)
-fun prefix_dt_names dt_descr sorts str = 
+fun prefix_dt_names descr sorts str = 
 let
   fun get_nth_name (i, _) = 
-    Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i) 
+    Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
 in
   Datatype_Prop.indexify_names 
-    (map (prefix str o get_nth_name) dt_descr)
+    (map (prefix str o get_nth_name) descr)
 end
 *}