--- 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 *)