diff -r c5232e6fb10b -r 3fb16bed5d6c src/HOL/Data_Structures/Set2_Join_RBT.thy
--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy	Tue Sep 24 17:36:14 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Wed Sep 25 17:22:57 2019 +0200
@@ -179,7 +179,7 @@
 by(cases "(l,a,r)" rule: baliR.cases) (auto simp: ball_Un)
 
 lemma bst_joinL:
-  "\<lbrakk>bst (Node l a n r); bheight l \<le> bheight r\<rbrakk>
+  "\<lbrakk>bst (Node l (a, n) r); bheight l \<le> bheight r\<rbrakk>
   \<Longrightarrow> bst (joinL l a r)"
 proof(induction l a r rule: joinL.induct)
   case (1 l a r)
@@ -202,7 +202,7 @@
 by(cases t) auto
 
 lemma bst_join:
-  "bst (Node l a n r) \<Longrightarrow> bst (join l a r)"
+  "bst (Node l (a, n) r) \<Longrightarrow> bst (join l a r)"
 by(auto simp: bst_paint bst_joinL bst_joinR join_def)
 
 lemma inv_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> invc(join l x r) \<and> invh(join l x r)"