src/HOL/ex/Quicksort.thy

--- a/src/HOL/ex/Quicksort.thy	Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/ex/Quicksort.thy	Tue May 08 10:14:36 2018 +0200
@@ -32,7 +32,7 @@
 qed
 
 lemma sorted_quicksort: "sorted (quicksort xs)"
-  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
+  by (induct xs rule: quicksort.induct) (auto simp add: sorted_append not_le less_imp_le)
 
 theorem sort_quicksort:
   "sort = quicksort"