diff -r 54e932f0c30a -r 4ec755485732 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Jul 19 16:50:39 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jul 20 13:51:38 2016 +0200
@@ -1612,7 +1612,7 @@
 lemma mset_insort [simp]: "mset (insort x xs) = mset xs + {#x#}"
   by (induct xs) (simp_all add: ac_simps)
 
-lemma mset_map: "mset (map f xs) = image_mset f (mset xs)"
+lemma mset_map[simp]: "mset (map f xs) = image_mset f (mset xs)"
   by (induct xs) simp_all
 
 global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"