diff -r 428d9cb9a243 -r 49ab06c0ca64 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Tue Aug 17 17:52:25 2010 +0800
@@ -41,12 +41,12 @@
   val fold_conj: term list -> term
 
   (* datatype operations *)
+  type cns_info = (term * typ * typ list * bool list) list
+
   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
   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 * bool list) list list
-  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
-    (term * typ * typ list * bool list) list
+  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list
+  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
   (* tactics for function package *)
@@ -130,6 +130,8 @@
 
 (** datatypes **)
 
+(* constructor infos *)
+type cns_info = (term * typ * typ list * bool list) list
 
 (* returns the type of the nth datatype *)
 fun all_dtyps descr sorts =