--- a/Nominal/Nominal2.thy	Tue Dec 06 23:42:19 2011 +0000
+++ b/Nominal/Nominal2.thy	Tue Dec 13 09:39:56 2011 +0000
@@ -172,14 +172,14 @@
   val lthy1 = Named_Target.theory_init thy1
 
   val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' 
-  val {descr, sorts, ...} = hd dtinfos
+  val {descr, ...} = hd dtinfos
 
-  val raw_tys = Datatype_Aux.get_rec_types descr sorts
+  val raw_tys = Datatype_Aux.get_rec_types descr
   val raw_ty_args = hd raw_tys
     |> snd o dest_Type
     |> map dest_TFree 
 
-  val raw_cns_info = all_dtyp_constrs_types descr sorts
+  val raw_cns_info = all_dtyp_constrs_types descr
   val raw_all_cns = (map o map) (fn (c, _, _, _) => c) raw_cns_info
 
   val raw_inject_thms = flat (map #inject dtinfos)

--- 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)