diff -r 5af6ed62385b -r ecd6f0ca62ea src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Mar 05 00:16:28 2009 +0100
+++ b/src/HOL/Library/Polynomial.thy	Wed Mar 04 17:12:23 2009 -0800
@@ -636,12 +636,14 @@
 begin
 
 primrec power_poly where
-  power_poly_0: "(p::'a poly) ^ 0 = 1"
-| power_poly_Suc: "(p::'a poly) ^ (Suc n) = p * p ^ n"
+  "(p::'a poly) ^ 0 = 1"
+| "(p::'a poly) ^ (Suc n) = p * p ^ n"
 
 instance
   by default simp_all
 
+declare power_poly.simps [simp del]
+
 end
 
 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"