--- a/Nominal/nominal_library.ML	Wed Jun 22 13:40:25 2011 +0100
+++ b/Nominal/nominal_library.ML	Wed Jun 22 14:14:54 2011 +0100
@@ -80,7 +80,6 @@
   (* datatype operations *)
   type cns_info = (term * typ * typ list * bool list) list
 
-  val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list
 
   (* tactics for function package *)
@@ -310,10 +309,6 @@
     - flags indicating whether the argument is recursive
 *)
 
-(* returns the type of the nth datatype *)
-fun all_dtyps descr sorts = 
-  map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))
-
 (* returns info about constructors in a datatype *)
 fun all_dtyp_constrs_info descr = 
   map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr