diff -r cfc795473656 -r b4b71c167e06 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Tue Dec 06 23:42:19 2011 +0000
+++ b/Nominal/nominal_library.ML	Tue Dec 13 09:39:56 2011 +0000
@@ -81,7 +81,7 @@
   (* datatype operations *)
   type cns_info = (term * typ * typ list * bool list) list
 
-  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list
+  val all_dtyp_constrs_types: Datatype_Aux.descr -> cns_info list
 
   (* tactics for function package *)
   val size_simpset: simpset
@@ -319,13 +319,13 @@
 
 (* returns the constants of the constructors plus the 
    corresponding type and types of arguments *)
-fun all_dtyp_constrs_types descr sorts = 
+fun all_dtyp_constrs_types descr = 
   let
     fun aux ((ty_name, vs), (cname, args)) =
       let
-        val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
+        val vs_tys = map (Datatype_Aux.typ_of_dtyp descr) vs
         val ty = Type (ty_name, vs_tys)
-        val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
+        val arg_tys = map (Datatype_Aux.typ_of_dtyp descr) args
         val is_rec = map Datatype_Aux.is_rec_type args
       in
         (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)