added sort_wrt;
authorwenzelm
Thu Oct 23 12:10:32 1997 +0200 (1997-10-23)
changeset 39731be726ef6813
parent 3972 87941982f475
child 3974 d3c2159b75fa
added sort_wrt;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Oct 23 12:09:48 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Oct 23 12:10:32 1997 +0200
     1.3 @@ -987,7 +987,8 @@
     1.4    in  sort1  end;
     1.5  
     1.6  (*sort strings*)
     1.7 -val sort_strings = sort (op <= : string * string -> bool);
     1.8 +fun sort_wrt sel xs = sort (op <= o pairself (sel: 'a -> string)) xs;
     1.9 +val sort_strings = sort_wrt I;
    1.10  
    1.11  
    1.12  (* transitive closure (not Warshall's algorithm) *)