# HG changeset patch
# User wenzelm
# Date 1149638494 -7200
# Node ID 46abcbb2da9dfc036d665d9229a95ff9425e2d94
# Parent  dae765e552ceceb3cd08d45bc0ce88d974460a13
added locale_insts;

diff -r dae765e552ce -r 46abcbb2da9d src/Pure/Isar/outer_parse.ML
--- 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" ||