
diff -r 09974789e483 -r 773b378d9313 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Oct 30 21:02:01 2014 +0100
@@ -790,7 +790,7 @@
     also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
       by (simp only: th)
     finally have ?case unfolding numeral_2_eq_2 [symmetric]
-    using odd_two_times_div_two_Suc [OF odd] by simp
+    using odd_two_times_div_two_nat [OF odd] by simp
   }
   moreover
   {




