diff -r 97ce525f664c -r e16f4baa3db6 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Mon Jul 14 17:51:48 2008 +0200
+++ b/src/HOL/Library/Quicksort.thy	Mon Jul 14 19:20:28 2008 +0200
@@ -17,13 +17,8 @@
 "quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
 by pat_completeness auto
 
-termination
-by (relation "measure size")
-   (auto simp: length_filter_le[THEN order_class.le_less_trans])
-
-end
-context linorder
-begin
+termination by (relation "measure size")
+  (auto simp: length_filter_le [THEN order_class.le_less_trans])
 
 lemma quicksort_permutes [simp]:
   "multiset_of (quicksort xs) = multiset_of xs"