pointer_eq_ord: minor performance tuning;

--- 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