--- 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;