# HG changeset patch
# User wenzelm
# Date 960148558 -7200
# Node ID 91cbae314c84a863e4c74468e3766779eb7a5888
# Parent  d9e09ef531ddee8a1a0862667b613a9a5d788e25
opt_mixfix', opt_infix';

diff -r d9e09ef531dd -r 91cbae314c84 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Jun 04 21:54:58 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 04 21:55:58 2000 +0200
@@ -105,7 +105,7 @@
 val typeabbrP =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
     (Scan.repeat1
-      (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)) -- P.marg_comment)
+      (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')) -- P.marg_comment)
       >> (Toplevel.theory o IsarThy.add_tyabbrs o
         map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
 
diff -r d9e09ef531dd -r 91cbae314c84 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sun Jun 04 21:54:58 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sun Jun 04 21:55:58 2000 +0200
@@ -49,6 +49,8 @@
   val typ: token list -> string * token list
   val opt_infix: token list -> Syntax.mixfix * token list
   val opt_mixfix: token list -> Syntax.mixfix * token list
+  val opt_infix': token list -> Syntax.mixfix * token list
+  val opt_mixfix': token list -> Syntax.mixfix * token list
   val const: token list -> (bstring * string * Syntax.mixfix) * token list
   val term: token list -> string * token list
   val prop: token list -> string * token list
@@ -212,11 +214,14 @@
   (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
   >> (Syntax.Mixfix o triple2);
 
-fun opt_fix fix =
-  Scan.optional ($$$ "(" |-- fix --| $$$ ")") Syntax.NoSyn;
+fun opt_fix guard fix =
+  Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn;
 
-val opt_infix = opt_fix (infxl || infxr);
-val opt_mixfix = opt_fix (mixfix || binder || infxl || infxr);
+val opt_infix = opt_fix !!! (infxl || infxr);
+val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr);
+
+val opt_infix' = opt_fix I (infxl || infxr);
+val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr);
 
 
 (* consts *)