src/HOL/BNF/BNF_LFP.thy
changeset 53309 42a99f732a40
parent 53305 29c267cb9314
child 53310 8af01463b2d3
--- 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: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"