src/HOL/BNF/BNF_LFP.thy

--- a/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:37:03 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:43:39 2013 +0200
@@ -10,7 +10,7 @@
 header {* Least Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_LFP
-imports BNF_FP_Basic
+imports BNF_FP_Base
 keywords
   "datatype_new" :: thy_decl and
   "datatype_new_compat" :: thy_decl and