diff -r 6fb86c61747c -r eba74a5790d2 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 18:16:22 2009 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 18:21:55 2009 +0200
@@ -85,13 +85,7 @@
 by (rule lemma_DERIV_subst, rule DERIV_add, auto)
 
 lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_pCons)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
-apply simp
-done
+  by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
 
 text{* Consequences of the derivative theorem above*}