# HG changeset patch
# User wenzelm
# Date 1004903849 -3600
# Node ID d6294ebfff24403334306619e01abe63b4e9c8e4
# Parent  8c86683597a8af9644f830f9630dced7442842a3
locale syntax;

diff -r 8c86683597a8 -r d6294ebfff24 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 04 20:56:59 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 04 20:57:29 2001 +0100
@@ -284,7 +284,10 @@
 
 (* statements *)
 
-val locale = Scan.option (P.$$$ "(" |-- P.!!! (P.$$$ "in" |-- P.xname --| P.$$$ ")"));
+val locale = Scan.optional (P.$$$ "(" |-- P.!!!
+    ((P.$$$ "in" |-- P.xname >> Some) -- Scan.repeat P.locale_element ||
+      Scan.repeat1 P.locale_element >> pair None) --| P.$$$ ")") (None, []);
+
 val statement = P.opt_thm_name ":" -- P.propp -- P.marg_comment;
 
 val theoremP =
@@ -700,10 +703,11 @@
 
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
-  "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
-  "files", "in", "infix", "infixl", "infixr", "is", "output", "overloaded",
-  "where", "|", "\\<equiv>", "\\<rightharpoonup>", "\\<leftharpoondown>",
-  "\\<rightleftharpoons>", "\\<subseteq>"];
+  "<=", "=", "==", "=>", "?", "[", "]", "and", "assumes", "binder",
+  "concl", "defines", "files", "fixes", "in", "infix", "infixl",
+  "infixr", "is", "notes", "output", "overloaded", "structure",
+  "uses", "where", "|", "\\<equiv>", "\\<leftharpoondown>",
+  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>"];
 
 val parsers = [
   (*theory structure*)