src/HOL/ex/Quicksort.thy

   "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
   by (simp_all add: not_le)
 
 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 -
   have "set_mset (mset (quicksort xs)) = set_mset (mset xs)"
     by simp