--- a/src/Pure/Pure.thy Wed Jan 29 11:53:49 2025 +0100
+++ b/src/Pure/Pure.thy Wed Jan 29 14:43:14 2025 +0100
@@ -1423,7 +1423,8 @@
local
val adhoc_overloading_args =
- Parse.and_list1 ((Parse.const --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) -- Scan.repeat Parse.term);
+ Parse.and_list1
+ ((Parse.const --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) -- Parse.!!! (Scan.repeat1 Parse.term));
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>adhoc_overloading\<close>