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 * string list) * token list
+  val locale_insts: token list ->
+    (string option list * ((bstring * Attrib.src list) * string) list) * token list
   val class_expr: token list -> string list * token list
   val locale_expr: 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
   val context_element: token list -> Element.context * token list

     >> (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.$$$ "where" |-- P.and_list1 P.term) [];
+  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
 
 local
 
 val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";