diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -439,11 +439,11 @@
 by (unfold deg_def) (fast intro: Least_le)
 
 lemma deg_aboveD:
-  assumes prem: "deg p < m" shows "coeff p m = 0"
+  assumes "deg p < m" shows "coeff p m = 0"
 proof -
   obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
   then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
-  then show "coeff p m = 0" by (rule boundD)
+  then show "coeff p m = 0" using `deg p < m` by (rule boundD)
 qed
 
 lemma deg_belowI:
@@ -470,7 +470,7 @@
     then have "EX m. deg p - 1 < m & coeff p m ~= 0"
       by (unfold bound_def) fast
     then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
-    then show ?thesis by auto 
+    then show ?thesis by (auto intro: that)
   qed
   with deg_belowI have "deg p = m" by fastsimp
   with m_coeff show ?thesis by simp