--- a/src/Pure/Isar/outer_parse.ML Wed Jun 07 02:01:33 2006 +0200
+++ b/src/Pure/Isar/outer_parse.ML Wed Jun 07 02:01:34 2006 +0200
@@ -82,6 +82,7 @@
((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_target: token list -> xstring * token list
val opt_locale_target: token list -> xstring option * token list
val locale_expr: token list -> Locale.expr * token list
@@ -349,6 +350,9 @@
and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- locale_mixfix >> (single o triple1) ||
params >> map Syntax.no_syn) >> flat;
+val locale_insts =
+ Scan.optional ($$$ "[" |-- !!! (Scan.repeat1 (maybe term) --| $$$ "]")) [];
+
local
val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" ||