# HG changeset patch # User wenzelm # Date 1310580807 -7200 # Node ID 9c9a9b13c5da000298cee2daa068a7c79dc62626 # Parent d5803c3d537a90d1dbbf83664252155193119d53 low-level tuning; diff -r d5803c3d537a -r 9c9a9b13c5da src/Pure/library.ML --- a/src/Pure/library.ML Wed Jul 13 16:42:14 2011 +0200 +++ b/src/Pure/library.ML Wed Jul 13 20:13:27 2011 +0200 @@ -908,7 +908,8 @@ 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); + if pointer_eq (s1, s2) then EQUAL + else (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