diff -r 79cebcc230d6 -r 231a20534950 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Sun Jun 06 13:16:27 2010 +0200
+++ b/Nominal/NewFv.thy	Mon Jun 07 11:33:00 2010 +0200
@@ -265,6 +265,8 @@
   val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
+  val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_bn_eqs)))
+
   fun pat_completeness_auto ctxt =
     Pat_Completeness.pat_completeness_tac ctxt 1
       THEN auto_tac (clasimpset_of ctxt)