--- a/src/HOL/Library/datatype_records.ML Mon Jan 13 12:11:25 2020 +0100
+++ b/src/HOL/Library/datatype_records.ML Tue Jan 14 16:03:31 2020 +0100
@@ -296,7 +296,7 @@
val parser =
(parse_ctr_options -- BNF_Util.parse_type_args_named_constrained -- Parse.binding) --
- (\<^keyword>\<open>=\<close> |-- Scan.repeat1 (Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ)))
+ (\<^keyword>\<open>=\<close> |-- Scan.repeat1 (Parse.binding -- (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.typ)))
val _ =
Outer_Syntax.local_theory
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Jan 13 12:11:25 2020 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Jan 14 16:03:31 2020 +0100
@@ -2379,12 +2379,12 @@
val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>friend_of_corec\<close>
"register a function as a legal context for nonprimitive corecursion"
- (Parse.const -- Scan.option (Parse.$$$ "::" |-- Parse.typ) --| Parse.where_ -- Parse.prop
+ (Parse.const -- Scan.option (\<^keyword>\<open>::\<close> |-- Parse.typ) --| Parse.where_ -- Parse.prop
>> friend_of_corec_cmd);
val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>coinduction_upto\<close>
"derive a coinduction up-to principle and a corresponding congruence closure"
- (Parse.name --| Parse.$$$ ":" -- Parse.typ >> coinduction_upto_cmd);
+ (Parse.name --| \<^keyword>\<open>:\<close> -- Parse.typ >> coinduction_upto_cmd);
val _ = Theory.setup (Theory.at_begin consolidate_global);