changeset 81170 | 2d73c3287bd3 |
parent 81148 | acd55a0d06f2 |
child 81533 | fb49af893986 |
--- a/src/Pure/Pure.thy Tue Oct 15 14:55:45 2024 +0200 +++ b/src/Pure/Pure.thy Tue Oct 15 14:57:23 2024 +0200 @@ -404,7 +404,7 @@ val syntax_consts = Parse.and_list1 - (Scan.optional (Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) [] -- + ((Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) -- Parse.!!! (Scan.repeat1 Parse.name_position)); val _ =