src/Pure/Isar/spec_parse.ML
changeset 25094 ba43514068fd
parent 24869 bad2b2be1f24
child 25999 f8bcd311d501
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Fri Oct 19 10:44:45 2007 +0200
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Fri Oct 19 12:21:32 2007 +0200
     1.3 @@ -23,7 +23,8 @@
     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 * string list) * token list
     1.8 +  val locale_insts: token list ->
     1.9 +    (string option list * ((bstring * Attrib.src list) * string) list) * token list
    1.10    val class_expr: token list -> string list * token list
    1.11    val locale_expr: token list -> Locale.expr * token list
    1.12    val locale_keyword: token list -> string * token list
    1.13 @@ -88,7 +89,7 @@
    1.14  
    1.15  val locale_insts =
    1.16    Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    1.17 -  -- Scan.optional (P.$$$ "where" |-- P.and_list1 P.term) [];
    1.18 +  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    1.19  
    1.20  local
    1.21