# HG changeset patch
# User wenzelm
# Date 1202558170 -3600
# Node ID f6f264ff2844f98303e1c2676a6956588fde5c7f
# Parent  d27b89c95b293c42f434f040d80cf122ceba7e45
overloading: tuned signature;

diff -r d27b89c95b29 -r f6f264ff2844 src/Pure/Isar/isar_syn.ML
--- 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)));