# HG changeset patch
# User blanchet
# Date 1473776592 -7200
# Node ID ce05cc93e07be03fa5a141827c189e4fd4db0bf6
# Parent  90360390a916a6aec7bef6536b90235e471f0478
union associates to the left

diff -r 90360390a916 -r ce05cc93e07b src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Sep 13 11:31:30 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Sep 13 16:23:12 2016 +0200
@@ -796,7 +796,7 @@
                 end;
             in
               if null set_apps then HOLogic.mk_set A []
-              else Library.foldr1 mk_union (map recurse set_apps)
+              else Library.foldl1 mk_union (map recurse set_apps)
             end
           | _ => HOLogic.mk_set A []));
   in build end;
diff -r 90360390a916 -r ce05cc93e07b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 13 11:31:30 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 13 16:23:12 2016 +0200
@@ -860,7 +860,7 @@
                   (filter (exists_subtype_in [A] o fastype_of) xs);
               in
                 mk_Trueprop_eq (setA $ list_comb (ctrA, xs),
-                  (if null sets then HOLogic.mk_set A [] else Library.foldr1 mk_union sets))
+                  (if null sets then HOLogic.mk_set A [] else Library.foldl1 mk_union sets))
               end;
 
             val goals =