diff -r ea2834adf8de -r 8ea9b7dec799 src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Sun Oct 06 19:33:58 2019 +0200
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Mon Oct 07 14:31:46 2019 +0200
@@ -36,19 +36,7 @@
 proof(induction t)
   case Leaf show ?case by (simp add: balanced_def)
 next
-  case (Node l x r)
-  have "size l = size r \<or> size l = size r + 1" (is "?A \<or> ?B")
-    using Node.prems by simp
-  thus ?case
-  proof
-    assume "?A"
-    thus ?thesis using Node
-      apply(simp add: balanced_def min_def max_def)
-      by (metis Node.IH balanced_optimal le_antisym le_refl)
-  next
-    assume "?B"
-    thus ?thesis using Node by(intro balanced_Node_if_wbal1) auto
-  qed
+  case (Node l x r) thus ?case using balanced_Node_if_wbal2 by force
 qed
 
 subsection \<open>Numbering Nodes\<close>