tuned mixfix syntax;
authorwenzelm
Sat, 01 Apr 2000 20:10:57 +0200
changeset 8648 7461dc59a818
parent 8647 656f1b61875a
child 8649 dc496bb0638f
tuned mixfix syntax;
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);