added where_;
authorwenzelm
Fri Nov 17 02:19:51 2006 +0100 (2006-11-17)
changeset 214004788fc8e66ea
parent 21399 700ae58d2273
child 21401 faddc6504177
added where_;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Nov 16 20:19:50 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Fri Nov 17 02:19:51 2006 +0100
     1.3 @@ -62,6 +62,7 @@
     1.4    val opt_mixfix: token list -> mixfix * token list
     1.5    val opt_infix': token list -> mixfix * token list
     1.6    val opt_mixfix': token list -> mixfix * token list
     1.7 +  val where_: token list -> string * token list
     1.8    val const: token list -> (string * string * mixfix) * token list
     1.9    val simple_fixes: token list -> (string * string option) list * token list
    1.10    val fixes: token list -> (string * string option * mixfix) list * token list
    1.11 @@ -267,6 +268,8 @@
    1.12  
    1.13  (* fixes *)
    1.14  
    1.15 +val where_ = $$$ "where";
    1.16 +
    1.17  val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    1.18  
    1.19  val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)