src/HOL/BNF/Tools/bnf_gfp.ML

       folded_dtor_set_thmss', dtor_Jrel_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
+  Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     (parse_datatype_cmd false construct_gfp);
 
 end;