--- a/Nominal/nominal_library.ML	Wed Jun 22 12:18:22 2011 +0100
+++ b/Nominal/nominal_library.ML	Wed Jun 22 13:40:25 2011 +0100
@@ -81,10 +81,7 @@
   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 -> 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 *)
   val size_simpset: simpset
@@ -317,9 +314,6 @@
 fun all_dtyps descr sorts = 
   map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))
 
-fun nth_dtyp descr sorts n = 
-  Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
-
 (* returns info about constructors in a datatype *)
 fun all_dtyp_constrs_info descr = 
   map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr
@@ -341,23 +335,6 @@
     map (map aux) (all_dtyp_constrs_info descr)
   end
 
-fun nth_dtyp_constrs_types descr sorts n =
-  nth (all_dtyp_constrs_types descr sorts) n
-
-
-(* generates for every datatype a name str ^ dt_name 
-   plus and index for multiple occurences of a string *)
-fun prefix_dt_names descr sorts str = 
-  let
-    fun get_nth_name (i, _) = 
-      Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
-  in
-    Datatype_Prop.indexify_names 
-      (map (prefix str o get_nth_name) descr)
-  end
-
-
-
 (** function package tactics **)
 
 fun pat_completeness_simp simps lthy =