--- a/src/Pure/Isar/isar_syn.ML Thu Feb 07 14:39:19 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Feb 09 12:56:10 2008 +0100
@@ -464,8 +464,8 @@
val _ =
OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
(Scan.repeat1 (P.name --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term --
- Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true)
- --| P.begin
+ Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
+ >> P.triple1) --| P.begin
>> (fn operations => Toplevel.print o
Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));