diff -r 8cedebf55539 -r 25aceefd4786 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Fri Jul 25 12:03:32 2008 +0200
+++ b/src/HOL/Library/Quicksort.thy	Fri Jul 25 12:03:34 2008 +0200
@@ -18,7 +18,7 @@
 by pat_completeness auto
 
 termination by (relation "measure size")
-  (auto simp: length_filter_le [THEN order_class.le_less_trans])
+  (auto simp: length_filter_le [THEN preorder_class.le_less_trans])
 
 lemma quicksort_permutes [simp]:
   "multiset_of (quicksort xs) = multiset_of xs"