# HG changeset patch
# User haftmann
# Date 1291412374 -3600
# Node ID 6c35a88d8f61f86100e53a686074d8bbdc7ca136
# Parent  a370b0fb6f099a6fe89faa03df33525f835229a9
tuned proposition

diff -r a370b0fb6f09 -r 6c35a88d8f61 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Fri Dec 03 22:34:20 2010 +0100
+++ b/src/HOL/Library/More_List.thy	Fri Dec 03 22:39:34 2010 +0100
@@ -85,16 +85,17 @@
   using assms by (induct xs) (auto simp add: o_assoc [symmetric])
 
 lemma fold_multiset_equiv:
-  assumes f: "\<And>x y. x \<in># multiset_of xs \<Longrightarrow> y \<in># multiset_of xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+  assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
     and equiv: "multiset_of xs = multiset_of ys"
   shows "fold f xs = fold f ys"
 using f equiv [symmetric] proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
 next
   case (Cons x xs)
+  then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD)
   have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
-    by (rule Cons.prems(1)) (simp_all add: mem_set_multiset_eq Cons.prems(2))
-  moreover from Cons.prems have "x \<in> set ys" by (simp add: mem_set_multiset_eq)
+    by (rule Cons.prems(1)) (simp_all add: *)
+  moreover from * have "x \<in> set ys" by simp
   ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
   moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
   ultimately show ?case by simp