diff -r 5cdcd51a4dad -r 28d1deca302e src/HOL/Data_Structures/Balance_List.thy
--- a/src/HOL/Data_Structures/Balance_List.thy	Wed Aug 10 18:57:20 2016 +0200
+++ b/src/HOL/Data_Structures/Balance_List.thy	Fri Aug 12 08:20:17 2016 +0200
@@ -5,7 +5,7 @@
 theory Balance_List
 imports
   "~~/src/HOL/Library/Tree"
-  "~~/src/HOL/Library/Float"
+  "~~/src/HOL/Library/Log_Nat"
 begin
 
 fun bal :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree * 'a list" where
@@ -73,7 +73,7 @@
     hence le: "?log2 \<le> ?log1" by(simp add:floorlog_mono)
     have "height t = max ?log1 ?log2 + 1" by (simp add: t IH1 IH2)
     also have "\<dots> = ?log1 + 1" using le by (simp add: max_absorb1)
-    also have "\<dots> = floorlog 2 n" by (simp add: Float.compute_floorlog)
+    also have "\<dots> = floorlog 2 n" by (simp add: compute_floorlog)
     finally show ?thesis .
   qed
 qed
@@ -106,7 +106,7 @@
     also have "\<dots> = floorlog 2 (n - n div 2)" by(simp add: floorlog_def)
     also have "n - n div 2 = (n+1) div 2" by arith
     also have "floorlog 2 \<dots> = floorlog 2 (n+1) - 1"
-      by (simp add: Float.compute_floorlog)
+      by (simp add: compute_floorlog)
     finally show ?thesis .
   qed
 qed