src/Pure/library.ML
changeset 16676 671bd433b9eb
parent 16654 d964cbaa6c1c
child 16688 e3de7ea24c23
     1.1 --- a/src/Pure/library.ML	Mon Jul 04 15:51:56 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Jul 04 17:07:10 2005 +0200
     1.3 @@ -232,6 +232,7 @@
     1.4    val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
     1.5    val int_ord: int * int -> order
     1.6    val string_ord: string * string -> order
     1.7 +  val fast_string_ord: string * string -> order
     1.8    val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
     1.9    val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
    1.10    val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
    1.11 @@ -1098,6 +1099,9 @@
    1.12  val int_ord = Int.compare;
    1.13  val string_ord = String.compare;
    1.14  
    1.15 +fun fast_string_ord (s1, s2) =
    1.16 +  (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2) | ord => ord);
    1.17 +
    1.18  fun option_ord ord (SOME x, SOME y) = ord (x, y)
    1.19    | option_ord _ (NONE, NONE) = EQUAL
    1.20    | option_ord _ (NONE, SOME _) = LESS
    1.21 @@ -1116,7 +1120,7 @@
    1.22  
    1.23  (*lexicographic product of lists*)
    1.24  fun list_ord elem_ord (xs, ys) =
    1.25 -  prod_ord int_ord (dict_ord elem_ord) ((length xs, xs), (length ys, ys));
    1.26 +  (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord);
    1.27  
    1.28  
    1.29  (* sorting *)