# HG changeset patch
# User wenzelm
# Date 1631039226 -7200
# Node ID bb37fb85d82ca2f88aa0d05620e47b020922158b
# Parent  6d48d6ba58df20e5bf7c1cb899ab155c01d9acb4
pointer_eq_ord: minor performance tuning;

diff -r 6d48d6ba58df -r bb37fb85d82c src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Tue Sep 07 17:13:34 2021 +0200
+++ b/src/Pure/term_ord.ML	Tue Sep 07 20:27:06 2021 +0200
@@ -34,12 +34,11 @@
 
 (* fast syntactic ordering -- tuned for inequalities *)
 
-fun fast_indexname_ord ((x, i), (y, j)) =
-  (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
+val fast_indexname_ord =
+  pointer_eq_ord (int_ord o apply2 snd ||| fast_string_ord o apply2 fst);
 
-fun sort_ord SS =
-  if pointer_eq SS then EQUAL
-  else dict_ord fast_string_ord SS;
+val sort_ord =
+  pointer_eq_ord (dict_ord fast_string_ord);
 
 local