--- 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 _ _ = [];