# HG changeset patch
# User wenzelm
# Date 1579014211 -3600
# Node ID 26801434d62897c024099d150fd08ab5e9ad7c62
# Parent  5ccf60c1f47c7c22a3284b1cbc4cec45a8d23e5a
more antiquotations;

diff -r 5ccf60c1f47c -r 26801434d628 src/HOL/Library/datatype_records.ML
--- 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
diff -r 5ccf60c1f47c -r 26801434d628 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- 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);