--- a/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 11 13:06:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 11 13:10:34 2012 +0200
@@ -1222,8 +1222,8 @@
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;