# HG changeset patch
# User wenzelm
# Date 1635705341 -3600
# Node ID 30eba7f9a8e9125c07ab58cfdc6ece419b6d7b87
# Parent  549019b4a808af1f8c4c36c3969c8f5255339e2c
minor performance tuning;

diff -r 549019b4a808 -r 30eba7f9a8e9 src/Pure/thm.ML
--- 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 *)