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