src/HOL/Library/Multiset.thy

 
 definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   "image_mset f = fold_mset (op + o single o f) {#}"
 
 interpretation image_left_comm: fun_left_comm "op + o single o f"
-proof qed (simp add: add_ac)
+proof qed (simp add: add_ac fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
 by (simp add: image_mset_def)
 
 lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"