# HG changeset patch
# User blanchet
# Date 1348404773 -7200
# Node ID b1bdbb099f9909942e3a57fe212ad4b1b474d383
# Parent  be6cbf960aa730cf56e9cf23b394ad9d8f51ed01
took out accidentally submitted "tracing" calls

diff -r be6cbf960aa7 -r b1bdbb099f99 src/HOL/BNF/Tools/bnf_fp_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -80,7 +80,6 @@
   let
     val ((Type (_, Ts0), Type (_, Us0)), body) =
       strip_type (fastype_of t) |>> split_last |>> apfst List.last;
-val _ = tracing ("*** " ^ PolyML.makestring (Ts, "***", Us, "***", t, Ts0, Us0)) (*###*)
   in
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   end;
@@ -933,7 +932,7 @@
               map5 (fn xctr => fn xs => fn sels =>
                 map2 (mk_goal threl xctr xs sels))) threls xctrss xsss selsss yctrss ysss;
 *)
-val _ = tracing ("goalsss: " ^ PolyML.makestring goalsss) (*###*)
+(* val _ = tracing ("goalsss: " ^ PolyML.makestring goalsss) (*###*) *)
           in
             ([], [])
           end;