diff -r d066e4923a31 -r 42a99f732a40 src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:09:51 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:12:41 2013 +0200 @@ -13,7 +13,7 @@ imports BNF_FP_Basic keywords "datatype_new" :: thy_decl and - "datatype_compat" :: thy_decl + "datatype_new_compat" :: thy_decl begin lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}"