# HG changeset patch
# User wenzelm
# Date 954612657 -7200
# Node ID 7461dc59a818e6e60d6e2424443588bb504403d8
# Parent  656f1b61875a72484940f19a3a50f5b949a80b38
tuned mixfix syntax;

diff -r 656f1b61875a -r 7461dc59a818 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sat Apr 01 20:09:52 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sat Apr 01 20:10:57 2000 +0200
@@ -209,11 +209,11 @@
 val opt_pris = Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [];
 
 val mixfix =
-  string -- opt_pris -- Scan.optional nat Syntax.max_pri
-  >> (Syntax.Mixfix o triple1);
+  (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
+  >> (Syntax.Mixfix o triple2);
 
 fun opt_fix fix =
-  Scan.optional ($$$ "(" |-- !!! (fix --| $$$ ")")) Syntax.NoSyn;
+  Scan.optional ($$$ "(" |-- fix --| $$$ ")") Syntax.NoSyn;
 
 val opt_infix = opt_fix (infxl || infxr);
 val opt_mixfix = opt_fix (mixfix || binder || infxl || infxr);