# HG changeset patch
# User wenzelm
# Date 1624009723 -7200
# Node ID aa0b1fbe6be3dc8c255afb219937540c56c3788d
# Parent  dfac078e5444e21e5bebe3d07c8143afc3b74606
tuned;

diff -r dfac078e5444 -r aa0b1fbe6be3 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Jun 18 11:32:32 2021 +0200
+++ b/src/Pure/library.ML	Fri Jun 18 11:48:43 2021 +0200
@@ -949,8 +949,8 @@
   | dict_ord _ (_ :: _, []) = GREATER;
 
 (*lexicographic product of lists*)
-fun list_ord elem_ord (xs, ys) =
-  (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord);
+fun length_ord (xs, ys) = int_ord (length xs, length ys);
+fun list_ord elem_ord = length_ord ||| dict_ord elem_ord;
 
 
 (* sorting *)