diff -r 00db0d934a7d -r 5398aa5a4df9 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:11:22 2015 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:17:29 2015 +0200
@@ -1217,7 +1217,7 @@
       then have "poly (polypoly' (?ts @ xs) p) = poly []"
         by auto
       then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
-        using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
+        using poly_zero[where ?'a='a] by (simp add: polypoly'_def)
       with coefficients_head[of p, symmetric]
       have th0: "Ipoly (?ts @ xs) ?hd = 0"
         by simp