diff -r 315694e22856 -r e85c24717cad src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/ex/Sorting.thy	Thu Jun 26 13:20:50 1997 +0200
@@ -21,7 +21,7 @@
 
 primrec sorted list
   "sorted le [] = True"
-  "sorted le (x#xs) = ((!y:set_of_list xs. le x y) & sorted le xs)"
+  "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
 
 primrec mset list
   "mset [] y = 0"