added sort_wrt;

--- a/src/Pure/library.ML	Thu Oct 23 12:09:48 1997 +0200
+++ b/src/Pure/library.ML	Thu Oct 23 12:10:32 1997 +0200
@@ -987,7 +987,8 @@
   in  sort1  end;
 
 (*sort strings*)
-val sort_strings = sort (op <= : string * string -> bool);
+fun sort_wrt sel xs = sort (op <= o pairself (sel: 'a -> string)) xs;
+val sort_strings = sort_wrt I;
 
 
 (* transitive closure (not Warshall's algorithm) *)