diff -r 028d5511c15f -r 72dfc74b6bd4 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue Jan 18 21:26:58 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jan 18 21:28:07 2011 +0100
@@ -531,7 +531,7 @@
       if eqvt_flag = false then NONE
       else 
         let
-          val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) 
+          (* val _ = tracing ("intrs:\n" ^ cat_lines (map @{make_string} intrs_gen)) *)
           val ([eqvt_thm], lthy) = Nominal_Eqvt.raw_equivariance false [Rdef] raw_induct intrs_gen lthy
         in
           SOME ((Nominal_ThmDecls.eqvt_transform lthy eqvt_thm) RS @{thm eqvtI})