union associates to the left

--- 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;

--- 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 =