# HG changeset patch
# User nipkow
# Date 1536820611 -7200
# Node ID 5d35fd21a0b9caeb4f12dad5453f054b1eada4e9
# Parent  b1d106c1edac6aacff142c0436dde133d70535ad
prefer explicit

diff -r b1d106c1edac -r 5d35fd21a0b9 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Sep 13 06:37:41 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 13 08:36:51 2018 +0200
@@ -1887,7 +1887,7 @@
 apply simp
 done
 
-lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
+lemma mset_compl_union: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
   by (induct xs) auto
 
 lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
diff -r b1d106c1edac -r 5d35fd21a0b9 src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Thu Sep 13 06:37:41 2018 +0200
+++ b/src/HOL/ex/Quicksort.thy	Thu Sep 13 08:36:51 2018 +0200
@@ -22,7 +22,7 @@
 
 lemma quicksort_permutes [simp]:
   "mset (quicksort xs) = mset xs"
-  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
+  by (induct xs rule: quicksort.induct) (simp_all add: mset_compl_union ac_simps)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
 proof -