# HG changeset patch
# User wenzelm
# Date 1544470508 -3600
# Node ID fc44536fa5059c07ee79572c679b5c7d26fd72a5
# Parent  0bd51c6aaa8b1cd614fbcf372afe564fa0e63bba
tuned proofs;

diff -r 0bd51c6aaa8b -r fc44536fa505 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Dec 10 20:20:24 2018 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Dec 10 20:35:08 2018 +0100
@@ -2615,7 +2615,7 @@
     @ sort_key f [x\<leftarrow>xs. f x > f (xs ! (length xs div 2))]" (is "sort_key f ?lhs = ?rhs")
 proof (rule properties_for_sort_key)
   show "mset ?rhs = mset ?lhs"
-    by (rule multiset_eqI) (auto simp add: mset_filter)
+    by (rule multiset_eqI) auto
   show "sorted (map f ?rhs)"
     by (auto simp add: sorted_append intro: sorted_map_same)
 next
@@ -3388,7 +3388,7 @@
   by simp
 
 lemma [code]: "filter_mset f (mset xs) = mset (filter f xs)"
-  by (simp add: mset_filter)
+  by simp
 
 lemma [code]: "mset xs - mset ys = mset (fold remove1 ys xs)"
   by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute diff_diff_add)