diff -r b283680d8044 -r d065b195ec89 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Oct 27 11:11:35 2010 -0700
+++ b/src/HOLCF/Fix.thy	Wed Oct 27 13:54:18 2010 -0700
@@ -119,7 +119,7 @@
 
 text {* strictness of @{term fix} *}
 
-lemma fix_defined_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
+lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
 apply (rule iffI)
 apply (erule subst)
 apply (rule fix_eq [symmetric])
@@ -127,10 +127,10 @@
 done
 
 lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
 
 lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
-by (simp add: fix_defined_iff)
+by (simp add: fix_bottom_iff)
 
 text {* @{term fix} applied to identity and constant functions *}