--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Sep 13 20:20:16 2015 +0200
@@ -891,7 +891,7 @@
subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution etc ...\<close>
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
-proof (induct p arbitrary: n rule: poly.induct, auto, goals)
+proof (induct p arbitrary: n rule: poly.induct, auto, goal_cases)
case prems: (1 c n p n')
then have "n = Suc (n - 1)"
by simp