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