P.context_element, P.locale_element;

--- a/src/Pure/Isar/isar_syn.ML	Wed Nov 09 16:26:50 2005 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 09 16:26:51 2005 +0100
@@ -302,8 +302,8 @@
 
 val locale_val =
   (P.locale_expr --
-    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.locale_element)) [] ||
-  Scan.repeat1 P.locale_element >> pair Locale.empty);
+    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
+  Scan.repeat1 P.context_element >> pair Locale.empty);
 
 val localeP =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
@@ -337,7 +337,7 @@
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
 val general_statement =
-  statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
+  statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
 
 fun gen_theorem kind =
   OuterSyntax.command kind ("state " ^ kind) K.thy_goal

--- a/src/Pure/Isar/outer_parse.ML	Wed Nov 09 16:26:50 2005 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Nov 09 16:26:51 2005 +0100
@@ -79,8 +79,8 @@
   val opt_locale_target: token list -> xstring option * token list
   val locale_expr: token list -> Locale.expr * token list
   val locale_keyword: token list -> string * token list
-  val locale_element: token list -> Locale.element * token list
-  val locale_elem_or_expr: token list -> Locale.element Locale.elem_expr * token list
+  val locale_element: token list -> Element.context Locale.element * token list
+  val context_element: token list -> Element.context * token list
   val method: token list -> Method.text * token list
 end;
 
@@ -321,7 +321,7 @@
 val name_facts = and_list1 (opt_thm_name "=" -- xthms1);
 
 
-(* locale elements *)
+(* locale and context elements *)
 
 local
 
@@ -331,15 +331,15 @@
 
 val loc_element =
   $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
-    >> triple1)) >> Locale.Fixes ||
+    >> triple1)) >> Element.Fixes ||
   $$$ "constrains" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ)))
-    >> Locale.Constrains ||
+    >> Element.Constrains ||
   $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
-    >> Locale.Assumes ||
+    >> Element.Assumes ||
   $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
-    >> Locale.Defines ||
+    >> Element.Defines ||
   $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
-    >> Locale.Notes;
+    >> Element.Notes;
 
 fun plus1 scan =
   scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
@@ -357,11 +357,10 @@
 val locale_expr = expr0;
 val locale_keyword = loc_keyword;
 
-val locale_element = group "locale element" loc_element;
+val locale_element = group "locale element"
+  (loc_element >> Locale.Elem || $$$ "includes" |-- !!! locale_expr >> Locale.Expr);
 
-val locale_elem_or_expr = group "locale element or includes"
-  (loc_element >> Locale.Elem ||
-  $$$ "includes" |-- !!! locale_expr >> Locale.Expr);
+val context_element = group "context element" loc_element;
 
 end;