src/HOL/Codatatype/BNF_LFP.thy

--- a/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 02:06:31 2012 +0200
+++ b/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 05:03:18 2012 +0200
@@ -8,9 +8,10 @@
 header {* Least Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_LFP
-imports BNF_Comp
+imports BNF_FP
 keywords
-  "data_raw" :: thy_decl
+  "data_raw" :: thy_decl and
+  "data" :: thy_decl
 uses
   "Tools/bnf_lfp_util.ML"
   "Tools/bnf_lfp_tactics.ML"