diff -r 27941d7d9a11 -r 40b411ec05aa src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Wed May 07 10:57:19 2008 +0200
@@ -227,7 +227,7 @@
 
 lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
 unfolding principal_less_iff
-by (simp add: less_def subset_def)
+by (simp add: less_def subset_eq)
 
 lemma lub_principal_approxes: "principal ` approxes x <<| x"
 apply (rule is_lubI)