diff -r 82f47e645c0a -r 8464b7f19c51 src/Pure/Pure.thy --- 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>\\\ || \<^keyword>\==\)) -- Scan.repeat Parse.term); + Parse.and_list1 + ((Parse.const --| (\<^keyword>\\\ || \<^keyword>\==\)) -- Parse.!!! (Scan.repeat1 Parse.term)); val _ = Outer_Syntax.local_theory \<^command_keyword>\adhoc_overloading\