Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 63862 ce05cc93e07b
parent 63859 dca6fabd8060
child 64067 6855c2f7aa6a 
--- 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 =
isabelle