src/HOL/BNF_Least_Fixpoint.thy

--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Mar 14 16:35:58 2019 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Mar 14 16:55:06 2019 +0100
@@ -12,8 +12,8 @@
 theory BNF_Least_Fixpoint
 imports BNF_Fixpoint_Base
 keywords
-  "datatype" :: thy_decl and
-  "datatype_compat" :: thy_decl
+  "datatype" :: thy_defn and
+  "datatype_compat" :: thy_defn
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"