src/Pure/Isar/spec_parse.ML
changeset 28710 e2064974c114
parent 28084 a05ca48ef263
child 28722 bdb694e18bf8
--- a/src/Pure/Isar/spec_parse.ML	Wed Oct 29 15:32:58 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Thu Oct 30 10:57:45 2008 +0100
@@ -27,11 +27,11 @@
   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 locale_element: token list -> Element.context * token list
   val context_element: token list -> Element.context * token list
   val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
   val general_statement: token list ->
-    (Element.context Locale.element list * Element.statement) * OuterLex.token list
+    (Element.context list * Element.statement) * OuterLex.token list
   val statement_keyword: token list -> string * token list
   val specification: token list ->
     (Name.binding *
@@ -120,8 +120,7 @@
 
 val locale_keyword = loc_keyword;
 
-val locale_element = P.group "locale element"
-  (loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr);
+val locale_element = P.group "locale element" loc_element;
 
 val context_element = P.group "context element" loc_element;