--- a/Nominal/Fv.thy	Thu Mar 11 11:25:18 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 11:25:56 2010 +0100
@@ -384,7 +384,7 @@
   val fv_names_all = fv_names_fst @ fv_bn_names;
   val add_binds = map (fn x => (Attrib.empty_binding, x))
 (* Function_Fun.add_fun Function_Common.default_config ... true *)
-  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)
+(*  val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*)
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
   val (fvs2, lthy'') =