1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:33:15 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:37:23 2012 +0200
     1.3 @@ -173,11 +173,9 @@
     1.4      fun mk_iter_like Ts Us t =
     1.5        let
     1.6          val (binders, body) = strip_type (fastype_of t);
     1.7 -val _ = tracing ("mk_iter_like: " ^ PolyML.makestring (binders, body, t)) (*###*)
     1.8          val (f_Us, prebody) = split_last binders;
     1.9          val Type (_, Ts0) = if lfp then prebody else body;
    1.10          val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
    1.11 -val _ = tracing (" Ts0 @ Us0 ...: " ^ PolyML.makestring (Ts0, Us0, Ts, Us)) (*###*)
    1.12        in
    1.13          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    1.14        end;
    1.15 @@ -376,7 +374,6 @@
    1.16  
    1.17              val [iter_def, rec_def] = map (Morphism.thm phi) defs;
    1.18  
    1.19 -val _ = tracing ("LFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*)
    1.20              val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.21            in
    1.22              ((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy)
    1.23 @@ -420,7 +417,6 @@
    1.24  
    1.25              val [coiter_def, corec_def] = map (Morphism.thm phi) defs;
    1.26  
    1.27 -val _ = tracing ("GFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*)
    1.28              val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.29            in
    1.30              ((ctrs, coiter, corec, v, xss, ctr_defs, coiter_def, corec_def), lthy)