--- a/src/HOL/HOLCF/UpperPD.thy Sat Mar 23 17:11:06 2013 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy Sat Mar 23 20:50:39 2013 +0100
@@ -302,7 +302,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
lemma ACI_upper_bind:
- "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
+ "semilattice (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
apply unfold_locales
apply (simp add: upper_plus_assoc)
apply (simp add: upper_plus_commute)