--- a/src/HOL/HOLCF/Domain_Aux.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Domain_Aux.thy Tue Jan 04 15:32:56 2011 -0800
@@ -52,7 +52,7 @@
have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
- then show ?thesis by (rule UU_I)
+ then show ?thesis by (rule bottomI)
qed
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"