# HG changeset patch
# User wenzelm
# Date 1682272306 -7200
# Node ID 6fcf3ca93dabc6cd0bbd04fc88311e3b53fc7b50
# Parent  a6bd716a61246f815d49da5ad43506349e4c59ab
tuned;

diff -r a6bd716a6124 -r 6fcf3ca93dab src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Sat Apr 22 21:00:24 2023 +0200
+++ b/src/Pure/General/set.ML	Sun Apr 23 19:51:46 2023 +0200
@@ -288,7 +288,7 @@
   else
     let
       fun elem_ord e = Key.ord (elem, e);
-      fun elem_less e = elem_ord e = LESS;
+      val elem_less = is_less o elem_ord;
 
       fun ins Empty = Sprout (Empty, elem, Empty)
         | ins (t as Leaf1 _) = ins (unmake t)