minimize theory imports

--- a/src/HOLCF/Algebraic.thy	Fri Oct 01 07:40:57 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Sat Oct 02 17:50:33 2010 -0700
@@ -5,7 +5,7 @@
 header {* Algebraic deflations *}
 
 theory Algebraic
-imports Completion Fix Eventual
+imports Completion Fix Eventual Bifinite
 begin
 
 subsection {* Constructing finite deflations by iteration *}

--- a/src/HOLCF/CompactBasis.thy	Fri Oct 01 07:40:57 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy	Sat Oct 02 17:50:33 2010 -0700
@@ -5,7 +5,7 @@
 header {* Compact bases of domains *}
 
 theory CompactBasis
-imports Completion
+imports Completion Bifinite
 begin
 
 subsection {* Compact bases of bifinite domains *}

--- a/src/HOLCF/Completion.thy	Fri Oct 01 07:40:57 2010 -0700
+++ b/src/HOLCF/Completion.thy	Sat Oct 02 17:50:33 2010 -0700
@@ -5,7 +5,7 @@
 header {* Defining bifinite domains by ideal completion *}
 
 theory Completion
-imports Bifinite
+imports Cfun
 begin
 
 subsection {* Ideals over a preorder *}