# HG changeset patch
# User berghofe
# Date 1210150773 -7200
# Node ID b4a24433154e89447692419967b8bb0f7efa8342
# Parent  9217577e0a23f9480c623775e5b9979f119c1d67
Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
it gets applied to sets as well.

diff -r 9217577e0a23 -r b4a24433154e src/HOL/Library/Multiset.thy
--- 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)