src/HOLCF/Ffun.thy

--- a/src/HOLCF/Ffun.thy	Tue Jul 01 01:28:44 2008 +0200
+++ b/src/HOLCF/Ffun.thy	Tue Jul 01 02:19:53 2008 +0200
@@ -92,7 +92,7 @@
 
 lemma thelub_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
-    \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
+    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
 by (rule lub_fun [THEN thelubI])
 
 lemma cpo_fun: