# HG changeset patch
# User wenzelm
# Date 1679947886 -7200
# Node ID 96a594e5e05429bb8de4042287d84ef25fbb648b
# Parent  b4032c468d7495dccec601851496f5ab91095d4c
added Set.size;
tuned Set.merge: keep larger set stable;

diff -r b4032c468d74 -r 96a594e5e054 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Mon Mar 27 21:53:16 2023 +0200
+++ b/src/Pure/General/set.ML	Mon Mar 27 22:11:26 2023 +0200
@@ -8,6 +8,7 @@
 sig
   type elem
   type T
+  val size: T -> int
   val empty: T
   val build: (T -> T) -> T
   val is_empty: T -> bool
@@ -37,6 +38,19 @@
   Branch3 of T * elem * T * elem * T;
 
 
+(* size *)
+
+local
+  fun add_size Empty n = n
+    | add_size (Branch2 (left, _, right)) n =
+        n + 1 |> add_size left |> add_size right
+    | add_size (Branch3 (left, _, mid, _, right)) n =
+        n + 2 |> add_size left |> add_size mid |> add_size right;
+in
+  fun size set = add_size set 0;
+end;
+
+
 (* empty and single *)
 
 val empty = Empty;
@@ -162,7 +176,10 @@
 fun merge (set1, set2) =
   if pointer_eq (set1, set2) then set1
   else if is_empty set1 then set2
-  else fold_set insert set2 set1;
+  else if is_empty set2 then set1
+  else if size set1 >= size set2
+  then fold_set insert set2 set1
+  else fold_set insert set1 set2;
 
 
 (* remove *)