clarified signature;

--- a/src/Pure/library.ML	Sat Aug 03 16:17:16 2019 +0200
+++ b/src/Pure/library.ML	Sat Aug 03 20:30:24 2019 +0200
@@ -8,6 +8,7 @@
 See also General/basics.ML for the most fundamental concepts.
 *)
 
+infixr 0 <<<
 infix 2 ?
 infix 3 o oo ooo oooo
 infix 4 ~~ upto downto
@@ -196,6 +197,7 @@
   val string_ord: string * string -> order
   val fast_string_ord: string * string -> order
   val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
+  val <<< : ('a -> order) * ('a -> order) -> 'a -> order
   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
   val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
@@ -904,6 +906,9 @@
   | rev_order EQUAL = EQUAL
   | rev_order GREATER = LESS;
 
+(*compose orders*)
+fun (a_ord <<< b_ord) p = (case a_ord p of EQUAL => b_ord p | ord => ord);
+
 (*assume rel is a linear strict order*)
 fun make_ord rel (x, y) =
   if rel (x, y) then LESS

--- a/src/Pure/more_thm.ML	Sat Aug 03 16:17:16 2019 +0200
+++ b/src/Pure/more_thm.ML	Sat Aug 03 20:30:24 2019 +0200
@@ -206,19 +206,11 @@
 
 (* thm order: ignores theory context! *)
 
-fun thm_ord ths =
-  (case Term_Ord.fast_term_ord (apply2 Thm.prop_of ths) of
-    EQUAL =>
-      (case
-        list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord)
-          (apply2 Thm.tpairs_of ths)
-       of
-        EQUAL =>
-          (case list_ord Term_Ord.fast_term_ord (apply2 Thm.hyps_of ths) of
-            EQUAL => list_ord Term_Ord.sort_ord (apply2 Thm.shyps_of ths)
-          | ord => ord)
-      | ord => ord)
-  | ord => ord);
+val thm_ord =
+  Term_Ord.fast_term_ord o apply2 Thm.prop_of
+  <<< list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of
+  <<< list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of
+  <<< list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of;
 
 
 (* tables and caches *)