src/Pure/Isar/isar_syn.ML
changeset 26048 f6f264ff2844
parent 25861 494d9301cc75
child 26184 64ee6a2ca6d6
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Feb 07 14:39:19 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Feb 09 12:56:10 2008 +0100
     1.3 @@ -464,8 +464,8 @@
     1.4  val _ =
     1.5    OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
     1.6     (Scan.repeat1 (P.name --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term --
     1.7 -      Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true)
     1.8 -        --| P.begin
     1.9 +      Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
    1.10 +      >> P.triple1) --| P.begin
    1.11     >> (fn operations => Toplevel.print o
    1.12           Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
    1.13