diff -r 21170e10c745 -r bdb694e18bf8 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Thu Nov 06 12:29:51 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Thu Nov 06 12:30:49 2008 +0100
@@ -27,7 +27,6 @@
   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 * 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 ->
@@ -88,9 +87,6 @@
 
 local
 
-val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
-   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
-
 val loc_element =
   P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
   P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
@@ -109,19 +105,18 @@
 
 in
 
-val class_expr = plus1_unless loc_keyword P.xname;
+val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
+   P.$$$ "defines" || P.$$$ "notes";
+
+val class_expr = plus1_unless locale_keyword P.xname;
 
 val locale_expr =
   let
     fun expr2 x = (P.xname >> Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
     and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x
-    and expr0 x = (plus1_unless loc_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
+    and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
   in expr0 end;
 
-val locale_keyword = loc_keyword;
-
-val locale_element = P.group "locale element" loc_element;
-
 val context_element = P.group "context element" loc_element;
 
 end;
@@ -137,7 +132,7 @@
 
 val general_statement =
   statement >> (fn x => ([], Element.Shows x)) ||
-  Scan.repeat locale_element --
+  Scan.repeat context_element --
    (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
     P.$$$ "shows" |-- P.!!! statement >> Element.Shows);