# HG changeset patch
# User wenzelm
# Date 1681288943 -7200
# Node ID c18c0dbefd55b7f3d9da254c056f50dcb024e3aa
# Parent  69ee23f83884e5bff9119cb2cce5c15957282af0
performance tuning: proper pointer_eq;

diff -r 69ee23f83884 -r c18c0dbefd55 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Wed Apr 12 09:18:36 2023 +0200
+++ b/src/Pure/term_items.ML	Wed Apr 12 10:42:23 2023 +0200
@@ -78,7 +78,7 @@
 fun make_set xs = build (fold add_set xs);
 
 fun subset (A: set, B: set) = forall (defined B o #1) A;
-fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
+fun eq_set (A: set, B: set) = pointer_eq (A, B) orelse size A = size B andalso subset (A, B);
 
 fun list_set_ord ord (Table tab) = tab |> Table.dest |> sort (ord o apply2 #2) |> map #1;
 val list_set = list_set_ord int_ord;