--- a/src/HOL/Library/Polynomial.thy Mon Apr 26 11:34:17 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Apr 26 11:34:19 2010 +0200
@@ -1093,10 +1093,10 @@
apply (cases "r = 0")
apply (cases "r' = 0")
apply (simp add: pdivmod_rel_def)
-apply (simp add: pdivmod_rel_def ring_simps degree_mult_eq)
+apply (simp add: pdivmod_rel_def field_simps degree_mult_eq)
apply (cases "r' = 0")
apply (simp add: pdivmod_rel_def degree_mult_eq)
-apply (simp add: pdivmod_rel_def ring_simps)
+apply (simp add: pdivmod_rel_def field_simps)
apply (simp add: degree_mult_eq degree_add_less)
done