1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Mar 17 14:01:09 2012 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Mar 17 15:33:08 2012 +0100
     1.3 @@ -1130,10 +1130,10 @@
     1.4  lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
     1.5    by (simp add: shift1_def)
     1.6  lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
     1.7 -  by (induct k arbitrary: p, auto simp add: shift1_degree)
     1.8 +  by (induct k arbitrary: p) (auto simp add: shift1_degree)
     1.9  
    1.10  lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
    1.11 -  by (induct n arbitrary: p, simp_all add: funpow_def)
    1.12 +  by (induct n arbitrary: p) (simp_all add: funpow.simps)
    1.13  
    1.14  lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
    1.15    by (induct p arbitrary: n rule: degree.induct, auto)