1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Jun 04 21:54:58 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 04 21:55:58 2000 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  val typeabbrP =
     1.5    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
     1.6      (Scan.repeat1
     1.7 -      (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)) -- P.marg_comment)
     1.8 +      (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')) -- P.marg_comment)
     1.9        >> (Toplevel.theory o IsarThy.add_tyabbrs o
    1.10          map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
    1.11  

     2.1 --- a/src/Pure/Isar/outer_parse.ML	Sun Jun 04 21:54:58 2000 +0200
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun Jun 04 21:55:58 2000 +0200
     2.3 @@ -49,6 +49,8 @@
     2.4    val typ: token list -> string * token list
     2.5    val opt_infix: token list -> Syntax.mixfix * token list
     2.6    val opt_mixfix: token list -> Syntax.mixfix * token list
     2.7 +  val opt_infix': token list -> Syntax.mixfix * token list
     2.8 +  val opt_mixfix': token list -> Syntax.mixfix * token list
     2.9    val const: token list -> (bstring * string * Syntax.mixfix) * token list
    2.10    val term: token list -> string * token list
    2.11    val prop: token list -> string * token list
    2.12 @@ -212,11 +214,14 @@
    2.13    (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
    2.14    >> (Syntax.Mixfix o triple2);
    2.15  
    2.16 -fun opt_fix fix =
    2.17 -  Scan.optional ($$$ "(" |-- fix --| $$$ ")") Syntax.NoSyn;
    2.18 +fun opt_fix guard fix =
    2.19 +  Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn;
    2.20  
    2.21 -val opt_infix = opt_fix (infxl || infxr);
    2.22 -val opt_mixfix = opt_fix (mixfix || binder || infxl || infxr);
    2.23 +val opt_infix = opt_fix !!! (infxl || infxr);
    2.24 +val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr);
    2.25 +
    2.26 +val opt_infix' = opt_fix I (infxl || infxr);
    2.27 +val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr);
    2.28  
    2.29  
    2.30  (* consts *)