# HG changeset patch
# User wenzelm
# Date 1120489630 -7200
# Node ID 671bd433b9eb7c94a6c0772fa7000361e2396946
# Parent  96bdc59afc0570cd171d5cf43bb3edff7f63ce7e
added fast_string_ord;

diff -r 96bdc59afc05 -r 671bd433b9eb src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jul 04 15:51:56 2005 +0200
+++ b/src/Pure/library.ML	Mon Jul 04 17:07:10 2005 +0200
@@ -232,6 +232,7 @@
   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   val int_ord: int * int -> order
   val string_ord: string * string -> order
+  val fast_string_ord: string * string -> order
   val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
   val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
@@ -1098,6 +1099,9 @@
 val int_ord = Int.compare;
 val string_ord = String.compare;
 
+fun fast_string_ord (s1, s2) =
+  (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2) | ord => ord);
+
 fun option_ord ord (SOME x, SOME y) = ord (x, y)
   | option_ord _ (NONE, NONE) = EQUAL
   | option_ord _ (NONE, SOME _) = LESS
@@ -1116,7 +1120,7 @@
 
 (*lexicographic product of lists*)
 fun list_ord elem_ord (xs, ys) =
-  prod_ord int_ord (dict_ord elem_ord) ((length xs, xs), (length ys, ys));
+  (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord);
 
 
 (* sorting *)