src/HOL/Data_Structures/RBT_Set.thy

     using rbt_height_bheight[OF assms] by (simp)
   also have "\<dots> \<le> size1 t" using assms
     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: Int.divide_le_eq_numeral1(1))
+    by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
   thus ?thesis by simp
 qed
 
 end