# HG changeset patch
# User wenzelm
# Date 1681837865 -7200
# Node ID 9374e13655e83f8bf9b17e66171abadb5c504280
# Parent  c274f52b11ffad9a04bb1a2043a3084363327085
drop unused Set().ord, which is potentially inefficient due to dict_ord/dest;

diff -r c274f52b11ff -r 9374e13655e8 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Apr 18 18:27:22 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Apr 18 19:11:05 2023 +0200
@@ -24,7 +24,6 @@
   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
   val merge: T * T -> T
@@ -238,7 +237,7 @@
   in get end;
 
 
-(* member *)
+(* member and subset *)
 
 fun member set elem =
   let
@@ -274,22 +273,11 @@
       | mem (Size (_, arg)) = mem arg;
   in mem set end;
 
-
-(* subset and order *)
-
 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
-      EQUAL =>
-        if subset sets then EQUAL
-        else dict_ord Key.ord (apply2 dest sets)
-    | ord => ord));
-
 
 (* insert *)