src/HOL/Library/Quicksort.thy
changeset 27682 25aceefd4786
parent 27580 e16f4baa3db6
child 28041 f496e9f343b7
--- 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"