src/Pure/Isar/outer_parse.ML
changeset 9037 91cbae314c84
parent 8897 fb1436ca3b2e
child 9131 cd17637c917f
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Sun Jun 04 21:54:58 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun Jun 04 21:55:58 2000 +0200
     1.3 @@ -49,6 +49,8 @@
     1.4    val typ: token list -> string * token list
     1.5    val opt_infix: token list -> Syntax.mixfix * token list
     1.6    val opt_mixfix: token list -> Syntax.mixfix * token list
     1.7 +  val opt_infix': token list -> Syntax.mixfix * token list
     1.8 +  val opt_mixfix': token list -> Syntax.mixfix * token list
     1.9    val const: token list -> (bstring * string * Syntax.mixfix) * token list
    1.10    val term: token list -> string * token list
    1.11    val prop: token list -> string * token list
    1.12 @@ -212,11 +214,14 @@
    1.13    (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
    1.14    >> (Syntax.Mixfix o triple2);
    1.15  
    1.16 -fun opt_fix fix =
    1.17 -  Scan.optional ($$$ "(" |-- fix --| $$$ ")") Syntax.NoSyn;
    1.18 +fun opt_fix guard fix =
    1.19 +  Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn;
    1.20  
    1.21 -val opt_infix = opt_fix (infxl || infxr);
    1.22 -val opt_mixfix = opt_fix (mixfix || binder || infxl || infxr);
    1.23 +val opt_infix = opt_fix !!! (infxl || infxr);
    1.24 +val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr);
    1.25 +
    1.26 +val opt_infix' = opt_fix I (infxl || infxr);
    1.27 +val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr);
    1.28  
    1.29  
    1.30  (* consts *)