diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOLCF/CompactBasis.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -46,7 +46,7 @@
 
 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
 
-interpretation compact_basis!:
+interpretation compact_basis:
   basis_take sq_le compact_take
 proof
   fix n :: nat and a :: "'a compact_basis"
@@ -92,7 +92,7 @@
   approximants :: "'a \<Rightarrow> 'a compact_basis set" where
   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
-interpretation compact_basis!:
+interpretation compact_basis:
   ideal_completion sq_le compact_take Rep_compact_basis approximants
 proof
   fix w :: 'a