# 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;