diff -r 93ef3ae2b9e5 -r 95d591908d8d src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Dec 19 11:09:31 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Fri Dec 19 11:57:21 2008 +0100
@@ -296,7 +296,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
+class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
   by unfold_locales
     (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+