# HG changeset patch
# User nipkow
# Date 1503762720 -7200
# Node ID 97c2d3846e10ac86fcb6deb22be9359fac2a57b8
# Parent  85c505c98332edd366fb255925a4e836837fa204
tuned

diff -r 85c505c98332 -r 97c2d3846e10 src/HOL/Data_Structures/Balance.thy
--- 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;