changeset 81010 | 5ea48342e0ae |
parent 80752 | 2c9b5288eb84 |
child 81106 | 849efff7de15 |
--- a/src/Pure/Pure.thy Sun Sep 29 21:20:36 2024 +0200 +++ b/src/Pure/Pure.thy Sun Sep 29 21:40:37 2024 +0200 @@ -404,7 +404,7 @@ val syntax_consts = Parse.and_list1 - ((Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) -- + (Scan.optional (Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) [] -- Parse.!!! (Scan.repeat1 Parse.name_position)); val _ =