# HG changeset patch
# User wenzelm
# Date 1681814701 -7200
# Node ID 92fd8bed5480f40748247faf8123ee75ac9420de
# Parent  1156aa9db7f5b4ec55601791ba655ead96a2e3bb
tuned whitespace;

diff -r 1156aa9db7f5 -r 92fd8bed5480 src/Pure/thm.ML
--- 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 *)