Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_function_core.ML
changeset 2677 72dfc74b6bd4
parent 2676 028d5511c15f
child 2707 747ebf2f066d 
--- 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})
nominal2