--- a/src/HOLCF/ConvexPD.thy Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/ConvexPD.thy Tue May 04 08:55:43 2010 +0200
@@ -412,7 +412,7 @@
(\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
lemma ACI_convex_bind:
- "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
+ "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
apply unfold_locales
apply (simp add: convex_plus_assoc)
apply (simp add: convex_plus_commute)