src/HOL/Library/Polynomial.thy

--- a/src/HOL/Library/Polynomial.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -1109,7 +1109,7 @@
 lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)"
   unfolding pos_poly_def
   apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
-  apply (simp add: degree_mult_eq coeff_mult_degree_sum mult_pos_pos)
+  apply (simp add: degree_mult_eq coeff_mult_degree_sum)
   apply auto
   done