# 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);