--- a/Nominal/Parser.thy	Mon May 03 11:43:08 2010 +0200
+++ b/Nominal/Parser.thy	Mon May 03 11:43:27 2010 +0200
@@ -483,7 +483,7 @@
   val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
-  val _ = map tracing (map PolyML.makestring alpha_eq_iff);
+(*  val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
   val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1