diff -r a5dc3558cdec -r 3b83960f9544 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Thu May 20 21:23:53 2010 +0100
@@ -6,6 +6,8 @@
 
 signature NOMINAL_LIBRARY =
 sig
+  val dest_listT: typ -> typ
+
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -25,12 +27,25 @@
 
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
+
+  (* datatype operations *)
+  val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
+  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
+    (term * typ * typ list) list list
+  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
+    (term * typ * typ list) list
+  val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
+
 end
 
 
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
+(* this function should be in hologic.ML *)
+fun dest_listT (Type (@{type_name list}, [T])) = T
+  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
+
 fun mk_minus p = @{term "uminus::perm => perm"} $ p;
 
 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;
@@ -59,6 +74,49 @@
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 
+(** datatypes **)
+
+
+(* returns the type of the nth datatype *)
+fun nth_dtyp descr sorts n = 
+  Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
+
+(* returns info about constructors in a datatype *)
+fun all_dtyp_constrs_info descr = 
+  map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr
+
+(* returns the constants of the constructors plus the 
+   corresponding type and types of arguments *)
+fun all_dtyp_constrs_types descr sorts = 
+let
+  fun aux ((ty_name, vs), (cname, args)) =
+  let
+    val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
+    val ty = Type (ty_name, vs_tys)
+    val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
+  in
+    (Const (cname, arg_tys ---> ty), ty, arg_tys)
+  end
+in
+  map (map aux) (all_dtyp_constrs_info descr)
+end
+
+fun nth_dtyp_constrs_types descr sorts n =
+  nth (all_dtyp_constrs_types descr sorts) n
+
+
+(* generates for every datatype a name str ^ dt_name 
+   plus and index for multiple occurences of a string *)
+fun prefix_dt_names descr sorts str = 
+let
+  fun get_nth_name (i, _) = 
+    Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
+in
+  Datatype_Prop.indexify_names 
+    (map (prefix str o get_nth_name) descr)
+end
+
+
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file