src/HOL/Codatatype/Tools/bnf_def.ML

   Outer_Syntax.improper_command @{command_spec "print_bnfs"} "print all BNFs"
     (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
-    (((Parse.binding --| Parse.$$$ "=") -- Parse.term --
-       (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
-       (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> bnf_def_cmd);
+    (((Parse.binding --| @{keyword "="}) -- Parse.term --
+       (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
+       (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd);
 
 end;