--- a/src/HOL/Library/Complete_Partial_Order2.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Fri May 13 20:24:10 2016 +0200
@@ -1552,7 +1552,7 @@
lemma mcont_SUP [cont_intro, simp]:
"\<lbrakk> mcont lub ord Union op \<subseteq> f; \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
-by(blast intro: mcontI cont_SUP[OF assms] monotone_SUP mcont_mono)
+by(blast intro: mcontI cont_SUP monotone_SUP mcont_mono)
end