# HG changeset patch
# User nipkow
# Date 1566232863 -7200
# Node ID b63e5e4598d7465998bb90a6639f18195d3f00f5
# Parent  e72daea2aab6b35e2ed9a848bbe70f4323f1440e
tuned

diff -r e72daea2aab6 -r b63e5e4598d7 src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Mon Aug 19 16:49:24 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Mon Aug 19 18:41:03 2019 +0200
@@ -85,9 +85,10 @@
 fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
 "split Leaf k = (Leaf, False, Leaf)" |
 "split (Node l a _ r) x =
-  (if x < a then let (l1,b,l2) = split l x in (l1, b, join l2 a r) else
-   if a < x then let (r1,b,r2) = split r x in (join l a r1, b, r2)
-   else (l, True, r))"
+  (case cmp x a of
+     LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) |
+     GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) |
+     EQ \<Rightarrow> (l, True, r))"
 
 lemma split: "split t x = (l,xin,r) \<Longrightarrow> bst t \<Longrightarrow>
   set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a}