diff -r 4278947ba336 -r 818898556504 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Sep 15 23:35:46 2018 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Sep 16 15:16:04 2018 +0200
@@ -299,7 +299,7 @@
     by (simp add: powr_realpow bheight_size_bound rbt_def)
   finally have "2 powr (height t / 2) \<le> size1 t" .
   hence "height t / 2 \<le> log 2 (size1 t)"
-    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
+    by (simp add: le_log_iff size1_size del: divide_le_eq_numeral1(1))
   thus ?thesis by simp
 qed