# HG changeset patch
# User blanchet
# Date 1347617367 -7200
# Node ID 9fa21648d0a197ee2ee8e8e320f34b1cc9c611c7
# Parent  be6e749fd003eb5ee395309c091f6a14a30104a0
put the flat at the right place (to avoid exceptions)

diff -r be6e749fd003 -r 9fa21648d0a1 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
@@ -561,9 +561,9 @@
                       val heads =
                         map2 (fn y => fn set => HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x)))
                           ys sets;
-                      val bodies = flat (map (mk_prem_prems names_lthy') ys);
+                      val bodiess = map (mk_prem_prems names_lthy') ys;
                     in
-                      map2 (curry Logic.mk_implies) heads bodies
+                      flat (map2 (map o curry Logic.mk_implies) heads bodiess)
                     end)
                 | i => [HOLogic.mk_Trueprop (nth phis i $ x)])
               | mk_prem_prems _ _ = [];