src/HOL/ex/Sorting.thy

--- a/src/HOL/ex/Sorting.thy	Thu Jan 16 16:53:15 1997 +0100
+++ b/src/HOL/ex/Sorting.thy	Fri Jan 17 10:04:28 1997 +0100
@@ -21,7 +21,7 @@
 sorted1_Cons "sorted1 f (Cons x (y#zs)) = (f x y & sorted1 f (y#zs))"
 
 sorted_Nil "sorted le []"
-sorted_Cons "sorted le (x#xs) = ((Alls y:xs. le x y) & sorted le xs)"
+sorted_Cons "sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)"
 
 mset_Nil "mset [] y = 0"
 mset_Cons "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"