src/HOL/BNF/Tools/bnf_fp_n2m.ML

--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 11:27:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Fri Aug 30 11:37:22 2013 +0200
@@ -374,9 +374,6 @@
         xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
        |> morph_fp_result (Morphism.term_morphism (singleton (Variable.polymorphic lthy))));
-(**
-    val _ = fp_res |> @{make_string} |> tracing
-**)
   in
     (fp_res, lthy)
   end