1.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Oct 29 15:32:58 2008 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Thu Oct 30 10:57:45 2008 +0100
     1.3 @@ -27,11 +27,11 @@
     1.4    val class_expr: token list -> string list * token list
     1.5    val locale_expr: token list -> Locale.expr * token list
     1.6    val locale_keyword: token list -> string * token list
     1.7 -  val locale_element: token list -> Element.context Locale.element * token list
     1.8 +  val locale_element: token list -> Element.context * token list
     1.9    val context_element: token list -> Element.context * token list
    1.10    val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
    1.11    val general_statement: token list ->
    1.12 -    (Element.context Locale.element list * Element.statement) * OuterLex.token list
    1.13 +    (Element.context list * Element.statement) * OuterLex.token list
    1.14    val statement_keyword: token list -> string * token list
    1.15    val specification: token list ->
    1.16      (Name.binding *
    1.17 @@ -120,8 +120,7 @@
    1.18  
    1.19  val locale_keyword = loc_keyword;
    1.20  
    1.21 -val locale_element = P.group "locale element"
    1.22 -  (loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr);
    1.23 +val locale_element = P.group "locale element" loc_element;
    1.24  
    1.25  val context_element = P.group "context element" loc_element;
    1.26