diff -r a02ea93e88c6 -r 893dcabf0c04 src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Mon Jun 28 15:32:17 2010 +0200
@@ -407,7 +407,7 @@
 
 lemma (in idom) poly_exp_eq_zero[simp]:
      "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
-apply (simp only: fun_eq add: all_simps [symmetric])
+apply (simp only: fun_eq add: HOL.all_simps [symmetric])
 apply (rule arg_cong [where f = All])
 apply (rule ext)
 apply (induct n)