diff -r 1264f2a21ea9 -r d7066575cbb9 Nominal/Nominal2.thy
--- 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