src/HOL/Library/Univ_Poly.thy

--- a/src/HOL/Library/Univ_Poly.thy	Tue Feb 28 17:11:18 2012 +0100
+++ b/src/HOL/Library/Univ_Poly.thy	Tue Feb 28 20:20:09 2012 +0100
@@ -103,7 +103,7 @@
 lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" by simp
 end
 
-lemma (in semiring_1) poly_ident_mult[simp]: "1 %* t = t" by (induct "t", auto)
+lemma (in semiring_1) poly_ident_mult[simp]: "1 %* t = t" by (induct t) auto
 
 lemma (in semiring_0) poly_simple_add_Cons[simp]: "[a] +++ ((0)#t) = (a#t)"
 by simp