diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Sep 13 11:13:15 2010 +0200
@@ -16,7 +16,7 @@
by auto
lemma expand_poly_eq: "p = q \ (\n. coeff p n = coeff q n)"
-by (simp add: coeff_inject [symmetric] ext_iff)
+by (simp add: coeff_inject [symmetric] fun_eq_iff)
lemma poly_ext: "(\n. coeff p n = coeff q n) \ p = q"
by (simp add: expand_poly_eq)
@@ -1403,7 +1403,7 @@
fixes p q :: "'a::{idom,ring_char_0} poly"
shows "poly p = poly q \ p = q"
using poly_zero [of "p - q"]
- by (simp add: ext_iff)
+ by (simp add: fun_eq_iff)
subsection {* Composition of polynomials *}