src/HOL/Codatatype/Tools/bnf_lfp.ML

     ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms, iter_thms, rec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations"
+  Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points of BNF equations"
     (Parse.and_list1
-      ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >>
+      ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
       (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
 
 end;