src/Pure/Isar/outer_parse.ML

   val mixfix: token list -> mixfix * token list
   val opt_infix: token list -> mixfix * token list
   val opt_mixfix: token list -> mixfix * token list
   val opt_infix': token list -> mixfix * token list
   val opt_mixfix': token list -> mixfix * token list
+  val where_: token list -> string * 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 for_fixes: token list -> (string * string option * mixfix) list * token list
   val for_simple_fixes: token list -> (string * string option) list * token list

 val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
 
 
 (* fixes *)
 
+val where_ = $$$ "where";
+
 val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
 
 val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)
   >> (fn (xs, T) => map (rpair T) xs);