--- a/Nominal/nominal_function_core.ML	Tue Jan 18 19:27:30 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jan 18 21:26:58 2011 +0100
@@ -531,6 +531,7 @@
       if eqvt_flag = false then NONE
       else 
         let
+          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})