# HG changeset patch
# User wenzelm
# Date 1150055965 -7200
# Node ID b8985bf2ce8bc1c3de6b1d9db3961bff1e2b84e8
# Parent  2c1fdc397ded78ac63833d0dbc24a94923d31cdb
added for_fixes;

diff -r 2c1fdc397ded -r b8985bf2ce8b src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sun Jun 11 21:59:24 2006 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sun Jun 11 21:59:25 2006 +0200
@@ -61,8 +61,9 @@
   val opt_infix': token list -> mixfix * token list
   val opt_mixfix': token list -> mixfix * token list
   val const: token list -> (string * string * mixfix) * token list
+  val simple_fixes: token list -> (string * string option) list * token list
   val fixes: token list -> (string * string option * mixfix) list * token list
-  val simple_fixes: token list -> (string * string option) list * token list
+  val for_fixes: token list -> (string * string option * mixfix) list * token list
   val term: token list -> string * token list
   val prop: token list -> string * token list
   val propp: token list -> (string * string list) * token list
@@ -269,6 +270,8 @@
   and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
     params >> map Syntax.no_syn) >> flat;
 
+val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
+
 
 (* terms *)