src/HOL/Decision_Procs/Polynomial_List.thy

--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -342,7 +342,7 @@
 
 lemma UNIV_nat_infinite: "\<not> finite (UNIV :: nat set)"
   unfolding finite_conv_nat_seg_image
-proof(auto simp add: expand_set_eq image_iff)
+proof(auto simp add: set_ext_iff image_iff)
   fix n::nat and f:: "nat \<Rightarrow> nat"
   let ?N = "{i. i < n}"
   let ?fN = "f ` ?N"