tuned

--- a/src/HOL/Data_Structures/Balance.thy	Sat Aug 26 16:47:25 2017 +0200
+++ b/src/HOL/Data_Structures/Balance.thy	Sat Aug 26 17:52:00 2017 +0200
@@ -7,8 +7,6 @@
   "HOL-Library.Tree_Real"
 begin
 
-(* FIXME rm floor_eq_iff / rename unique \<rightarrow> eq *)
-
 fun bal :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree * 'a list" where
 "bal n xs = (if n=0 then (Leaf,xs) else
  (let m = n div 2;