tuning

--- 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;

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 13:06:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 11 13:10:34 2012 +0200
@@ -682,10 +682,10 @@
     prepare_datatype Syntax.read_typ info specs fake_lthy lthy
   end;
 
-val parse_opt_binding_colon = Scan.optional (Parse.binding --| Parse.$$$ ":") no_binder
+val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
 
 val parse_ctr_arg =
-  Parse.$$$ "(" |-- parse_opt_binding_colon -- Parse.typ --| Parse.$$$ ")" ||
+  @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
   (Parse.typ >> pair no_binder);
 
 val parse_single_spec =

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 11 13:06:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 11 13:10:34 2012 +0200
@@ -3006,9 +3006,9 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points for BNF equations"
+  Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest 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_gfp o apsnd split_list o split_list));
 
 end;

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

--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 11 13:06:14 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 11 13:10:34 2012 +0200
@@ -513,8 +513,8 @@
   |> (fn thms => after_qed thms lthy)) oo
   prepare_wrap_datatype (K I) (* FIXME? (singleton o Type_Infer_Context.infer_types) *)
 
-val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]";
-val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";
+val parse_bindings = @{keyword "["} |-- Parse.list Parse.binding --| @{keyword "]"};
+val parse_bindingss = @{keyword "["} |-- Parse.list parse_bindings --| @{keyword "]"};
 
 val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
@@ -522,7 +522,7 @@
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
-    (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
+    (((@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
       Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], []))
      >> wrap_datatype_cmd);