diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -20,7 +20,7 @@
 lemma convex_le_trans: "\<lbrakk>t \<le>\<natural> u; u \<le>\<natural> v\<rbrakk> \<Longrightarrow> t \<le>\<natural> v"
 unfolding convex_le_def by (fast intro: upper_le_trans lower_le_trans)
 
-interpretation convex_le!: preorder convex_le
+interpretation convex_le: preorder convex_le
 by (rule preorder.intro, rule convex_le_refl, rule convex_le_trans)
 
 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<natural> t"
@@ -178,7 +178,7 @@
 unfolding convex_principal_def
 by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
 
-interpretation convex_pd!:
+interpretation convex_pd:
   ideal_completion convex_le pd_take convex_principal Rep_convex_pd
 apply unfold_locales
 apply (rule pd_take_convex_le)