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