# HG changeset patch # User blanchet # Date 1347133043 -7200 # Node ID 60a0394d98f78ecb4f864d0c5b1a74bc0d2b28a0 # Parent f43d28683679d95f9f95d0f435d51411236c14de oops diff -r f43d28683679 -r 60a0394d98f7 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:33:15 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:37:23 2012 +0200 @@ -173,11 +173,9 @@ fun mk_iter_like Ts Us t = let val (binders, body) = strip_type (fastype_of t); -val _ = tracing ("mk_iter_like: " ^ PolyML.makestring (binders, body, t)) (*###*) val (f_Us, prebody) = split_last binders; val Type (_, Ts0) = if lfp then prebody else body; val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us); -val _ = tracing (" Ts0 @ Us0 ...: " ^ PolyML.makestring (Ts0, Us0, Ts, Us)) (*###*) in Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; @@ -376,7 +374,6 @@ val [iter_def, rec_def] = map (Morphism.thm phi) defs; -val _ = tracing ("LFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*) val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts; in ((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy) @@ -420,7 +417,6 @@ val [coiter_def, corec_def] = map (Morphism.thm phi) defs; -val _ = tracing ("GFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*) val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts; in ((ctrs, coiter, corec, v, xss, ctr_defs, coiter_def, corec_def), lthy)