diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -2555,7 +2555,7 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
+  Outer_Syntax.local_theory @{command_keyword codatatype} "define coinductive datatypes"
     (parse_co_datatype_cmd Greatest_FP construct_gfp);
 
 val _ = Theory.setup (fp_antiquote_setup @{binding codatatype});