diff -r dd7992d4a61a -r 01fbfb60c33e src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:37:06 2014 +0100
@@ -406,7 +406,7 @@
   { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
     assume "\<forall>m\<in>set ms. m > 0"
     then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
-      by (induct ms) (auto, metis Suc_pred' case_nat_Suc) }
+      by (induct ms) (auto, metis Suc_pred' nat.cases(2)) }
   note * = this
   show ?thesis
     by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
@@ -452,7 +452,7 @@
 lemma coeff_Poly_eq:
   "coeff (Poly xs) n = nth_default 0 xs n"
   apply (induct xs arbitrary: n) apply simp_all
-  by (metis case_nat_0 case_nat_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
+  by (metis nat.cases not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
 
 lemma nth_default_coeffs_eq:
   "nth_default 0 (coeffs p) = coeff p"