src/HOL/Library/Multiset.thy
changeset 61890 f6ded81f5690
parent 61832 e15880ba58ac
child 61955 e96292f32c3c
--- 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 "\<lambda>x M. {#x#} + M" "{#}"
+global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
   defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}"
   by standard (simp add: fun_eq_iff ac_simps)