1.1 --- a/src/HOL/Library/Multiset.thy	Sat Aug 20 23:35:30 2011 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Aug 20 23:36:18 2011 +0200
     1.3 @@ -1598,7 +1598,7 @@
     1.4  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
     1.5    "image_mset f = fold_mset (op + o single o f) {#}"
     1.6  
     1.7 -interpretation image_fun_commute: comp_fun_commute "op + o single o f"
     1.8 +interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
     1.9  proof qed (simp add: add_ac fun_eq_iff)
    1.10  
    1.11  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"