--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Mar 06 14:15:09 2014 +0100
@@ -8,7 +8,7 @@
header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
theory BNF_Cardinal_Order_Relation
-imports BNF_Constructions_on_Wellorders
+imports Zorn BNF_Constructions_on_Wellorders
begin
text{* In this section, we define cardinal-order relations to be minim well-orders
--- a/src/HOL/BNF_Comp.thy Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Thu Mar 06 14:15:09 2014 +0100
@@ -8,7 +8,7 @@
header {* Composition of Bounded Natural Functors *}
theory BNF_Comp
-imports Basic_BNFs
+imports BNF_Def
begin
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
--- a/src/HOL/BNF_FP_Base.thy Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Thu Mar 06 14:15:09 2014 +0100
@@ -10,7 +10,7 @@
header {* Shared Fixed Point Operations on Bounded Natural Functors *}
theory BNF_FP_Base
-imports BNF_Comp
+imports BNF_Comp Basic_BNFs
begin
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
--- a/src/HOL/BNF_Wellorder_Embedding.thy Thu Mar 06 14:14:54 2014 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Thu Mar 06 14:15:09 2014 +0100
@@ -8,7 +8,7 @@
header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}
theory BNF_Wellorder_Embedding
-imports Zorn BNF_Wellorder_Relation
+imports Hilbert_Choice BNF_Wellorder_Relation
begin
text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and