new theory header syntax.

--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 16 14:22:27 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 16 17:06:47 2004 +0200
@@ -754,8 +754,8 @@
 
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
-  "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
-  "binder", "concl", "defines", "files", "fixes", "in", "includes",
+  "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
+  "binder", "concl", "defines", "files", "fixes", "import", "in", "includes",
   "infix", "infixl", "infixr", "is", "notes", "open", "output",
   "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
   "\\<leftharpoondown>", "\\<rightharpoonup>",

--- a/src/Pure/Isar/thy_header.ML	Mon Aug 16 14:22:27 2004 +0200
+++ b/src/Pure/Isar/thy_header.ML	Mon Aug 16 17:06:47 2004 +0200
@@ -56,16 +56,17 @@
 
 (* scan old/new headers *)
 
-val header_lexicon =
-  T.make_lexicon ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN];
+val header_lexicon = T.make_lexicon
+  ["(", ")", "+", ":", ";", "=", "begin", "files", headerN, "import", theoryN];
 
 val file_name =
   (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
 
-
 val args =
-  (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
-    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|  P.$$$ ":")
+  (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name ||
+              P.$$$ "import" |-- Scan.repeat1 P.name) --
+    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|
+  (P.$$$ ":" || P.$$$ "begin"))
   >> (fn ((A, Bs), files) => (A, Bs, files));