diff -r f18b8e8a4909 -r 7c8242a02f39 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Apr 30 14:48:13 2010 +0200
+++ b/Nominal/Parser.thy	Fri Apr 30 15:45:39 2010 +0200
@@ -428,7 +428,6 @@
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = tracing "Proving respects";
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
-  val _ = map tracing (map PolyML.makestring bns_rsp_pre')
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;