--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 22 12:18:22 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 22 13:40:25 2011 +0100
@@ -4,15 +4,6 @@
 
 section {*** Type Schemes ***}
 
-datatype foo =
-  Foo1
-| Foo2 bar
-and bar =
-  Bar
-
-ML {* #induct (Datatype_Data.the_info @{theory} "TypeSchemes.bar") *}
-
-
 atom_decl name 
 
 (* defined as a single nominal datatype *)

--- a/Nominal/Nominal2.thy	Wed Jun 22 12:18:22 2011 +0100
+++ b/Nominal/Nominal2.thy	Wed Jun 22 13:40:25 2011 +0100
@@ -193,12 +193,11 @@
   val {descr, sorts, ...} = dtinfo
 
   val raw_tys = all_dtyps descr sorts
-  val raw_full_ty_names = map (fst o dest_Type) raw_tys
   val tvs = hd raw_tys
     |> snd o dest_Type
     |> map dest_TFree  
 
-  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names  
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_dt_names  
  
   val raw_cns_info = all_dtyp_constrs_types descr sorts
   val raw_constrs = (map o map) (fn (c, _, _, _) => c) raw_cns_info
@@ -215,14 +214,14 @@
   
   val _ = trace_msg (K "Defining raw permutations...")
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
-    define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0
+    define_raw_perms raw_dt_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0
  
   (* noting the raw permutations as eqvt theorems *)
   val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 
   val _ = trace_msg (K "Defining raw fv- and bn-functions...")
   val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
-    define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
+    define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     
   (* defining the permute_bn functions *)
@@ -231,12 +230,12 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a
     
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = 
-    define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
+    define_raw_fvs raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
     
   val _ = trace_msg (K "Defining alpha relations...")
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
-    define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
+    define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
     
   val alpha_tys = map (domain_type o fastype_of) alpha_trms  
 

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