src/HOL/HOLCF/Fix.thy

--- a/src/HOL/HOLCF/Fix.thy	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Fix.thy	Tue Jan 04 15:32:56 2011 -0800
@@ -122,7 +122,7 @@
 apply (rule iffI)
 apply (erule subst)
 apply (rule fix_eq [symmetric])
-apply (erule fix_least [THEN UU_I])
+apply (erule fix_least [THEN bottomI])
 done
 
 lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"