--- a/Nominal/Fv.thy	Tue Mar 23 09:56:29 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 23 11:42:06 2010 +0100
@@ -841,14 +841,13 @@
 
 ML {*
 fun equivp_tac reflps symps transps =
-  let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in
+  (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
   simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
   THEN' rtac conjI THEN' rtac allI THEN'
   resolve_tac reflps THEN'
   rtac conjI THEN' rtac allI THEN' rtac allI THEN'
   resolve_tac symps THEN'
   rtac @{thm transpI} THEN' resolve_tac transps
-  end
 *}
 
 ML {*