diff -r d3f2038198ae -r a3cc9fa1295d src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Wed Mar 31 18:18:03 2021 +0200
@@ -94,7 +94,27 @@
 proof(induction t arbitrary: l b r rule: tree2_induct)
   case Leaf thus ?case by simp
 next
-  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
+  case (Node y a b z l c r)
+  consider (LT) l1 xin l2 where "(l1,xin,l2) = split y x" 
+    and "split \<langle>y, (a, b), z\<rangle> x = (l1, xin, join l2 a z)" and "cmp x a = LT"
+  | (GT) r1 xin r2 where "(r1,xin,r2) = split z x" 
+    and "split \<langle>y, (a, b), z\<rangle> x = (join y a r1, xin, r2)" and "cmp x a = GT"
+  | (EQ) "split \<langle>y, (a, b), z\<rangle> x = (y, True, z)" and "cmp x a = EQ"
+    by (force split: cmp_val.splits prod.splits if_splits)
+
+  thus ?case 
+  proof cases
+    case (LT l1 xin l2)
+    with Node.IH(1)[OF \<open>(l1,xin,l2) = split y x\<close>[symmetric]] Node.prems
+    show ?thesis by (force intro!: bst_join)
+  next
+    case (GT r1 xin r2)
+    with Node.IH(2)[OF \<open>(r1,xin,r2) = split z x\<close>[symmetric]] Node.prems
+    show ?thesis by (force intro!: bst_join)
+  next
+    case EQ
+    with Node.prems show ?thesis by auto
+  qed
 qed
 
 lemma split_inv: "split t x = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"