--- a/src/Pure/thm.ML Sat Oct 30 21:11:18 2021 +0200
+++ b/src/Pure/thm.ML Sun Oct 31 19:35:41 2021 +0100
@@ -532,10 +532,11 @@
(* thm order: ignores theory context! *)
val thm_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;
+ 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);
(* implicit theory context *)