diff -r 30d0b2f1df76 -r a79c1080f1e9 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Mar 02 21:16:02 2017 +0100
+++ b/src/HOL/Library/Float.thy	Sun Mar 05 10:57:51 2017 +0100
@@ -1646,7 +1646,7 @@
       powr_realpow[symmetric] powr_mult_base)
 
   have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
-    by (auto simp: field_simps powr_add powr_mult_base powr_numeral powr_divide2[symmetric] abs_mult)
+    by (auto simp: field_simps powr_add powr_mult_base powr_divide2[symmetric] abs_mult)
   also have "\<dots> \<le> 2 powr 0"
     using H by (intro powr_mono) auto
   finally have abs_m2_less_half: "\<bar>?m2\<bar> < 1 / 2"
@@ -1657,7 +1657,7 @@
   also have "\<dots> \<le> 2 powr real_of_int (e1 - e2 - 2)"
     by simp
   finally have b_less_quarter: "\<bar>?b\<bar> < 1/4 * 2 powr real_of_int e1"
-    by (simp add: powr_add field_simps powr_divide2[symmetric] powr_numeral abs_mult)
+    by (simp add: powr_add field_simps powr_divide2[symmetric] abs_mult)
   also have "1/4 < \<bar>real_of_int m1\<bar> / 2" using \<open>m1 \<noteq> 0\<close> by simp
   finally have b_less_half_a: "\<bar>?b\<bar> < 1/2 * \<bar>?a\<bar>"
     by (simp add: algebra_simps powr_mult_base abs_mult)