src/Pure/library.ML
changeset 3973 1be726ef6813
parent 3874 552ce5ad6a2e
child 4046 f89dbf002604
     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) *)