--- a/Nominal/NewParser.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/NewParser.thy	Thu May 27 18:37:52 2010 +0200
@@ -358,6 +358,7 @@
   val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt'
   val ths = Variable.export ctxt' ctxt ths_loc
   val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+  val _ = tracing ("eqvt thms\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) ths))
 in
   (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
 end