| changeset 44617 | 5db68864a967 |
| parent 43793 | 9c9a9b13c5da |
| child 45626 | b4f374a45668 |
--- a/src/Pure/library.ML Thu Sep 01 13:39:40 2011 +0200 +++ b/src/Pure/library.ML Thu Sep 01 14:10:52 2011 +0200 @@ -959,7 +959,7 @@ fun sort_distinct ord = quicksort true ord; val sort_strings = sort string_ord; -fun sort_wrt sel xs = sort (string_ord o pairself sel) xs; +fun sort_wrt key xs = sort (string_ord o pairself key) xs; (* items tagged by integer index *)