diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -1350,7 +1350,7 @@
       also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
         using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
         by (simp only: real_of_float_minus real_of_int_minus real_of_one
-            number_of_Min diff_minus mult_minus_left mult_1_left)
+            minus_one [symmetric] diff_minus mult_minus_left mult_1_left)
       also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
         unfolding real_of_float_minus cos_minus ..
       also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1394,7 +1394,7 @@
       also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
         using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
         by (simp only: real_of_float_minus real_of_int_minus real_of_one
-          number_of_Min diff_minus mult_minus_left mult_1_left)
+          minus_one [symmetric] diff_minus mult_minus_left mult_1_left)
       also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
         using lb_cos[OF lx_0 pi_lx] by simp
       finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -2117,7 +2117,8 @@
 lemma interpret_floatarith_num:
   shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
   and "interpret_floatarith (Num (Float 1 0)) vs = 1"
-  and "interpret_floatarith (Num (Float (number_of a) 0)) vs = number_of a" by auto
+  and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a"
+  and "interpret_floatarith (Num (Float (neg_numeral a) 0)) vs = neg_numeral a" by auto
 
 subsection "Implement approximation function"