--- a/Nominal/nominal_dt_alpha.ML	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Mon Dec 06 14:24:17 2010 +0000
@@ -247,6 +247,8 @@
       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
     val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
 
+    val _ = tracing ("alpha in def\n" ^ cat_lines (map (@{make_string} o fst o #1) all_alpha_names))
+
     val (alphas, lthy') = Inductive.add_inductive_i
        {quiet_mode = true, verbose = false, alt_name = Binding.empty,
         coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}