added locale_insts;
authorwenzelm
Wed Jun 07 02:01:34 2006 +0200 (2006-06-07)
changeset 1981146abcbb2da9d
parent 19810 dae765e552ce
child 19812 60c6bfbf6ca1
added locale_insts;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Jun 07 02:01:33 2006 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Jun 07 02:01:34 2006 +0200
     1.3 @@ -82,6 +82,7 @@
     1.4      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
     1.5    val locale_mixfix: token list -> mixfix * token list
     1.6    val locale_fixes: token list -> (string * string option * mixfix) list * token list
     1.7 +  val locale_insts: token list -> string option list * token list
     1.8    val locale_target: token list -> xstring * token list
     1.9    val opt_locale_target: token list -> xstring option * token list
    1.10    val locale_expr: token list -> Locale.expr * token list
    1.11 @@ -349,6 +350,9 @@
    1.12    and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- locale_mixfix >> (single o triple1) ||
    1.13      params >> map Syntax.no_syn) >> flat;
    1.14  
    1.15 +val locale_insts =
    1.16 +  Scan.optional ($$$ "[" |-- !!! (Scan.repeat1 (maybe term) --| $$$ "]")) [];
    1.17 +
    1.18  local
    1.19  
    1.20  val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" ||