--- a/src/HOL/Library/Polynomial.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Tue Sep 07 10:05:19 2010 +0200
@@ -16,7 +16,7 @@
by auto
lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
-by (simp add: coeff_inject [symmetric] expand_fun_eq)
+by (simp add: coeff_inject [symmetric] ext_iff)
lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> 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 \<longleftrightarrow> p = q"
using poly_zero [of "p - q"]
- by (simp add: expand_fun_eq)
+ by (simp add: ext_iff)
subsection {* Composition of polynomials *}