--- a/src/HOL/ex/Quicksort.thy	Thu Sep 13 15:15:50 2018 +0200
+++ b/src/HOL/ex/Quicksort.thy	Thu Sep 13 16:15:05 2018 +0200
@@ -22,7 +22,7 @@
 
 lemma quicksort_permutes [simp]:
   "mset (quicksort xs) = mset xs"
-  by (induct xs rule: quicksort.induct) (simp_all add: mset_compl_union ac_simps)
+by (induction xs rule: quicksort.induct) (simp_all)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
 proof -