src/Pure/Isar/outer_parse.ML
changeset 19845 b8985bf2ce8b
parent 19811 46abcbb2da9d
child 20273 ea313e02fd13
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Sun Jun 11 21:59:24 2006 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun Jun 11 21:59:25 2006 +0200
     1.3 @@ -61,8 +61,9 @@
     1.4    val opt_infix': token list -> mixfix * token list
     1.5    val opt_mixfix': token list -> mixfix * token list
     1.6    val const: token list -> (string * string * mixfix) * token list
     1.7 +  val simple_fixes: token list -> (string * string option) list * token list
     1.8    val fixes: token list -> (string * string option * mixfix) list * token list
     1.9 -  val simple_fixes: token list -> (string * string option) list * token list
    1.10 +  val for_fixes: token list -> (string * string option * mixfix) list * token list
    1.11    val term: token list -> string * token list
    1.12    val prop: token list -> string * token list
    1.13    val propp: token list -> (string * string list) * token list
    1.14 @@ -269,6 +270,8 @@
    1.15    and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
    1.16      params >> map Syntax.no_syn) >> flat;
    1.17  
    1.18 +val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
    1.19 +
    1.20  
    1.21  (* terms *)
    1.22