tuned signature (see 2d6a489adb01);

--- a/src/Pure/library.ML	Thu Jun 17 12:57:22 2021 +0200
+++ b/src/Pure/library.ML	Fri Jun 18 11:32:32 2021 +0200
@@ -8,7 +8,7 @@
 See also General/basics.ML for the most fundamental concepts.
 *)
 
-infixr 0 <<<
+infixr 0 |||
 infix 2 ?
 infix 3 o oo ooo oooo
 infix 4 ~~ upto downto
@@ -199,7 +199,7 @@
   val string_ord: string ord
   val fast_string_ord: string ord
   val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
-  val <<< : ('a -> order) * ('a -> order) -> 'a -> 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
@@ -913,7 +913,7 @@
   | rev_order GREATER = LESS;
 
 (*compose orders*)
-fun (a_ord <<< b_ord) p = (case a_ord p of EQUAL => b_ord p | ord => ord);
+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) =

--- a/src/Pure/more_thm.ML	Thu Jun 17 12:57:22 2021 +0200
+++ b/src/Pure/more_thm.ML	Fri Jun 18 11:32:32 2021 +0200
@@ -207,9 +207,9 @@
 
 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;
+  ||| 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 *)

--- a/src/Pure/thm.ML	Thu Jun 17 12:57:22 2021 +0200
+++ b/src/Pure/thm.ML	Fri Jun 18 11:32:32 2021 +0200
@@ -378,8 +378,8 @@
 
 val constraint_ord : constraint ord =
   Context.theory_id_ord o apply2 (Context.theory_id o #theory)
-  <<< Term_Ord.typ_ord o apply2 #typ
-  <<< Term_Ord.sort_ord o apply2 #sort;
+  ||| Term_Ord.typ_ord o apply2 #typ
+  ||| Term_Ord.sort_ord o apply2 #sort;
 
 val smash_atyps =
   map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T);
@@ -867,8 +867,8 @@
     type key = string * sort list * class;
     val ord =
       fast_string_ord o apply2 #1
-      <<< fast_string_ord o apply2 #3
-      <<< list_ord Term_Ord.sort_ord o apply2 #2;
+      ||| fast_string_ord o apply2 #3
+      ||| list_ord Term_Ord.sort_ord o apply2 #2;
   );
 
 datatype classes = Classes of