# HG changeset patch
# User wenzelm
# Date 877601432 -7200
# Node ID 1be726ef681327ed8f721f4b4bbd4c395effb628
# Parent  87941982f4754227faf66e41b7faf186f515d0ed
added sort_wrt;

diff -r 87941982f475 -r 1be726ef6813 src/Pure/library.ML
--- 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) *)