--- a/src/Pure/Isar/spec_parse.ML Fri Apr 13 10:00:04 2007 +0200
+++ b/src/Pure/Isar/spec_parse.ML Fri Apr 13 10:01:43 2007 +0200
@@ -23,7 +23,8 @@
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
val locale_mixfix: token list -> mixfix * token list
val locale_fixes: token list -> (string * string option * mixfix) list * token list
- val locale_insts: token list -> string option list * token list
+ val locale_insts: token list ->
+ (string option list * (string * string) list) * token list
val locale_expr: token list -> Locale.expr * token list
val locale_expr_unless: (token list -> 'a * token list) ->
token list -> Locale.expr * token list
@@ -86,7 +87,8 @@
P.params >> map Syntax.no_syn) >> flat;
val locale_insts =
- Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
+ Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
+ -- Scan.optional (P.$$$ "where" |-- P.and_list1 (P.term -- (P.$$$ "=" |-- P.!!! P.term))) [];
local