src/HOL/BNF_Wellorder_Embedding.thy

--- 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