tuned;
authorwenzelm
Fri, 18 Jun 2021 11:48:43 +0200
changeset 74117 aa0b1fbe6be3
parent 74116 dfac078e5444
child 74118 38fe15a42ff2
tuned;
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 *)