--- a/src/Pure/General/set.ML Wed Apr 12 10:42:23 2023 +0200
+++ b/src/Pure/General/set.ML Wed Apr 12 10:52:50 2023 +0200
@@ -23,6 +23,7 @@
val get_first: (elem -> 'a option) -> T -> 'a option
val member: T -> elem -> bool
val subset: T * T -> bool
+ val eq_set: T * T -> bool
val ord: T ord
val insert: elem -> T -> T
val make: elem list -> T
@@ -278,6 +279,9 @@
fun subset (set1, set2) = forall (member set2) set1;
+fun eq_set (set1, set2) =
+ pointer_eq (set1, set2) orelse size set1 = size set2 andalso subset (set1, set2);
+
val ord =
pointer_eq_ord (fn sets =>
(case int_ord (apply2 size sets) of