minor performance tuning;

--- a/src/Pure/library.ML	Fri May 05 11:36:56 2023 +0200
+++ b/src/Pure/library.ML	Fri May 05 11:47:38 2023 +0200
@@ -963,15 +963,17 @@
   | dict_ord _ ([], _ :: _) = LESS
   | dict_ord _ (_ :: _, []) = GREATER;
 
-(*lexicographic product of lists*)
-fun length_ord (xs, ys) = int_ord (length xs, length ys);
-fun list_ord elem_ord = length_ord ||| dict_ord elem_ord;
+fun length_ord args =
+  (case args of
+    (_ :: xs, _ :: ys) => length_ord (xs, ys)
+  | ([], []) => EQUAL
+  | ([], _ :: _) => LESS
+  | (_ :: _, []) => GREATER);
 
-fun vector_ord ord =
-  pointer_eq_ord (int_ord o apply2 Vector.length ||| Vector.collate ord);
-
-fun array_ord ord =
-  pointer_eq_ord (int_ord o apply2 Array.length ||| Array.collate ord);
+(*lexicographic product of lists, vectors, arrays*)
+fun list_ord elem_ord = length_ord ||| dict_ord elem_ord;
+fun vector_ord ord = pointer_eq_ord (int_ord o apply2 Vector.length ||| Vector.collate ord);
+fun array_ord ord = pointer_eq_ord (int_ord o apply2 Array.length ||| Array.collate ord);
 
 
 (* sorting *)