diff -r 51526dd8da8e -r e90d9d51106b src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/CompactBasis.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -47,8 +46,8 @@
 
 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
 
-interpretation compact_basis:
-  basis_take [sq_le compact_take]
+interpretation compact_basis!:
+  basis_take sq_le compact_take
 proof
   fix n :: nat and a :: "'a compact_basis"
   show "compact_take n a \<sqsubseteq> a"
@@ -93,8 +92,8 @@
   approximants :: "'a \<Rightarrow> 'a compact_basis set" where
   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
-interpretation compact_basis:
-  ideal_completion [sq_le compact_take Rep_compact_basis approximants]
+interpretation compact_basis!:
+  ideal_completion sq_le compact_take Rep_compact_basis approximants
 proof
   fix w :: 'a
   show "preorder.ideal sq_le (approximants w)"
@@ -245,7 +244,7 @@
   assumes "ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
-  interpret ab_semigroup_idem_mult [f] by fact
+  interpret ab_semigroup_idem_mult f by fact
   show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 qed