--- a/src/Pure/thm.ML Tue Apr 18 12:23:37 2023 +0200
+++ b/src/Pure/thm.ML Tue Apr 18 12:45:01 2023 +0200
@@ -541,10 +541,10 @@
val thm_ord =
pointer_eq_ord
- (Term_Ord.fast_term_ord o apply2 prop_of
- ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of
- ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of
- ||| list_ord Term_Ord.sort_ord o apply2 shyps_of);
+ (Term_Ord.fast_term_ord o apply2 prop_of
+ ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of
+ ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of
+ ||| list_ord Term_Ord.sort_ord o apply2 shyps_of);
(* implicit theory context *)