Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
it gets applied to sets as well.

--- a/src/HOL/Library/Multiset.thy	Wed May 07 10:59:32 2008 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed May 07 10:59:33 2008 +0200
@@ -196,7 +196,7 @@
 by (auto simp add: set_of_def)
 
 lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
-by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
+by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq [where f="Rep_multiset M"])
 
 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
 by (auto simp add: set_of_def)