diff -r 4e04f38329e5 -r eda5aeb056a6 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Jun 22 14:14:54 2011 +0100
+++ b/Nominal/Nominal2.thy	Thu Jun 23 11:30:39 2011 +0100
@@ -239,7 +239,7 @@
 
   val _ = trace_msg (K "Proving distinct theorems...")
   val alpha_distincts = 
-    mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
+    mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names
 
   val _ = trace_msg (K "Proving eq-iff theorems...")
   val alpha_eq_iff = 
@@ -287,7 +287,7 @@
   val _ = trace_msg (K "Proving alpha implies bn...")
   val alpha_bn_imp_thms = 
     raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 
-  
+
   val _ = trace_msg (K "Proving respectfulness...")
   val raw_funs_rsp_aux = 
     raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs