# HG changeset patch
# User wenzelm
# Date 1163726391 -3600
# Node ID 4788fc8e66ea5e40233817ae20a1a1727a9ab201
# Parent  700ae58d2273106a7ef22eca483700ccd12c0c73
added where_;

diff -r 700ae58d2273 -r 4788fc8e66ea src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Nov 16 20:19:50 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Nov 17 02:19:51 2006 +0100
@@ -62,6 +62,7 @@
   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
@@ -267,6 +268,8 @@
 
 (* fixes *)
 
+val where_ = $$$ "where";
+
 val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
 
 val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)