diff -r bc263f1f68cd -r dfac078e5444 src/Pure/more_thm.ML
--- 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 *)