src/Pure/Isar/spec_parse.ML

   val xthms1: token list -> (thmref * Attrib.src list) list * token list
   val name_facts: token list ->
     ((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
   val locale_keyword: token list -> string * token list
   val locale_element: token list -> Element.context Locale.element * token list

   P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
     >> (single o P.triple1) ||
   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
 
 val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";