src/HOLCF/Pcpo.thy

--- a/src/HOLCF/Pcpo.thy	Tue Sep 07 10:05:19 2010 +0200
+++ b/src/HOLCF/Pcpo.thy	Tue Sep 07 12:04:18 2010 +0200
@@ -89,7 +89,7 @@
 lemma lub_equal:
   "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
-  by (simp only: expand_fun_eq [symmetric])
+  by (simp only: ext_iff [symmetric])
 
 lemma lub_eq:
   "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"