tuned;

--- 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)