diff -r b915a10a616a -r c74270fd72a8 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Jun 20 22:41:41 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Fri Jun 20 22:51:50 2008 +0200
@@ -493,7 +493,7 @@
   show "\<exists>n. compact_approx n a = a"
     apply (simp add: Rep_compact_basis_inject [symmetric])
     apply (simp add: Rep_compact_approx)
-    apply (rule bifinite_compact_eq_approx)
+    apply (rule profinite_compact_eq_approx)
     apply (rule compact_Rep_compact_basis)
     done
 qed
@@ -523,8 +523,8 @@
       apply simp
       apply (cut_tac a=x in compact_Rep_compact_basis)
       apply (cut_tac a=y in compact_Rep_compact_basis)
-      apply (drule bifinite_compact_eq_approx)
-      apply (drule bifinite_compact_eq_approx)
+      apply (drule profinite_compact_eq_approx)
+      apply (drule profinite_compact_eq_approx)
       apply (clarify, rename_tac i j)
       apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
       apply (simp add: compact_le_def)