# HG changeset patch
# User wenzelm
# Date 1681908523 -7200
# Node ID 2cd00c4054abca45dab94bf891f421ab547f913e
# Parent  bb7238e7d2d90c17e43dbef077a6a7a99f8240dc
minor performance tuning: recursive check of pointer_eq;

diff -r bb7238e7d2d9 -r 2cd00c4054ab src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Wed Apr 19 14:29:52 2023 +0200
+++ b/src/Pure/term_ord.ML	Wed Apr 19 14:48:43 2023 +0200
@@ -62,38 +62,54 @@
   | cons_nr (Abs _) = 4
   | cons_nr (_ $ _) = 5;
 
-fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
-  | struct_ord (t1 $ t2, u1 $ u2) =
-      (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
-  | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
+fun struct_ord tu =
+  if pointer_eq tu then EQUAL
+  else
+    (case tu of
+      (Abs (_, _, t), Abs (_, _, u)) => struct_ord (t, u)
+    | (t1 $ t2, u1 $ u2) =>
+        (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
+    | (t, u) => int_ord (cons_nr t, cons_nr u));
 
-fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
-  | atoms_ord (t1 $ t2, u1 $ u2) =
-      (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
-  | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
-  | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
-  | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
-  | atoms_ord (Bound i, Bound j) = int_ord (i, j)
-  | atoms_ord _ = EQUAL;
+fun atoms_ord tu =
+  if pointer_eq tu then EQUAL
+  else
+    (case tu of
+      (Abs (_, _, t), Abs (_, _, u)) => atoms_ord (t, u)
+    | (t1 $ t2, u1 $ u2) =>
+        (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
+    | (Const (a, _), Const (b, _)) => fast_string_ord (a, b)
+    | (Free (x, _), Free (y, _)) => fast_string_ord (x, y)
+    | (Var (xi, _), Var (yj, _)) => fast_indexname_ord (xi, yj)
+    | (Bound i, Bound j) => int_ord (i, j)
+    | _ => EQUAL);
 
-fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
-      (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
-  | types_ord (t1 $ t2, u1 $ u2) =
-      (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
-  | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
-  | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
-  | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
-  | types_ord _ = EQUAL;
+fun types_ord tu =
+  if pointer_eq tu then EQUAL
+  else
+    (case tu of
+      (Abs (_, T, t), Abs (_, U, u)) =>
+        (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
+    | (t1 $ t2, u1 $ u2) =>
+        (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
+    | (Const (_, T), Const (_, U)) => typ_ord (T, U)
+    | (Free (_, T), Free (_, U)) => typ_ord (T, U)
+    | (Var (_, T), Var (_, U)) => typ_ord (T, U)
+    | _ => EQUAL);
 
-fun comments_ord (Abs (x, _, t), Abs (y, _, u)) =
-      (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord)
-  | comments_ord (t1 $ t2, u1 $ u2) =
-      (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord)
-  | comments_ord _ = EQUAL;
+fun comments_ord tu =
+  if pointer_eq tu then EQUAL
+  else
+    (case tu of
+      (Abs (x, _, t), Abs (y, _, u)) =>
+        (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord)
+    | (t1 $ t2, u1 $ u2) =>
+        (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord)
+    | _ => EQUAL);
 
 in
 
-val fast_term_ord = pointer_eq_ord (struct_ord ||| atoms_ord ||| types_ord);
+val fast_term_ord = struct_ord ||| atoms_ord ||| types_ord;
 
 val syntax_term_ord = fast_term_ord ||| comments_ord;