diff -r 542f2c6da692 -r f6ded81f5690 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Dec 18 14:23:11 2015 +0100 +++ b/src/HOL/Library/Multiset.thy Sat Dec 19 11:05:04 2015 +0100 @@ -1054,7 +1054,7 @@ lemma mset_map: "mset (map f xs) = image_mset f (mset xs)" by (induct xs) simp_all -permanent_interpretation mset_set: folding "\x M. {#x#} + M" "{#}" +global_interpretation mset_set: folding "\x M. {#x#} + M" "{#}" defines mset_set = "folding.F (\x M. {#x#} + M) {#}" by standard (simp add: fun_eq_iff ac_simps)