src/HOL/BNF/BNF_Util.thy

--- a/src/HOL/BNF/BNF_Util.thy	Thu Nov 14 19:54:10 2013 +0100
+++ b/src/HOL/BNF/BNF_Util.thy	Thu Nov 14 20:55:09 2013 +0100
@@ -9,7 +9,7 @@
 header {* Library for Bounded Natural Functors *}
 
 theory BNF_Util
-imports Ctr_Sugar "../Cardinals/Cardinal_Arithmetic"
+imports "../Cardinals/Cardinal_Arithmetic"
 begin
 
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"