src/HOL/HOLCF/Universal.thy

     by (rule exI, rule inj_place)
 qed
 
 end
 
-interpretation compact_basis!:
+interpretation compact_basis:
   ideal_completion below Rep_compact_basis
     "approximants :: 'a::bifinite \<Rightarrow> 'a compact_basis set"
 proof -
   obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a"
     using bifinite ..