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