# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268303156 -3600
# Node ID 0310a21821a7d99d1b5cff50d100acfb09084f13
# Parent  137cad9c1ce9e4b6f5f2f425821c2361f4ea4978
Remove tracing from fv/alpha.

diff -r 137cad9c1ce9 -r 0310a21821a7 Nominal/Fv.thy
--- 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'') =