# HG changeset patch
# User wenzelm
# Date 1124192566 -7200
# Node ID 5e9c1b81b690638c13d0f4e1df806dbce4dd3404
# Parent  f6284547701bb319511bf3c9a52dff700b04a646
P.tags;

diff -r f6284547701b -r 5e9c1b81b690 src/Pure/Isar/thy_header.ML
--- a/src/Pure/Isar/thy_header.ML	Tue Aug 16 13:42:45 2005 +0200
+++ b/src/Pure/Isar/thy_header.ML	Tue Aug 16 13:42:46 2005 +0200
@@ -59,7 +59,7 @@
 (* scan old/new headers *)
 
 val header_lexicon = T.make_lexicon
-  ["(", ")", "+", ":", ";", "=", beginN, filesN, headerN, importsN, theoryN, usesN];
+  ["%", "(", ")", "+", ":", ";", "=", beginN, filesN, headerN, importsN, theoryN, usesN];
 
 val file =
   (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
@@ -68,14 +68,14 @@
 val args =
   P.name --
    (P.$$$ "=" |-- P.!!! (P.enum1 "+" P.name -- files (P.$$$ filesN) --| P.$$$ ":") ||
-    P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- files (P.$$$ filesN || P.$$$ usesN)
-      --| P.$$$ beginN))
+    P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- files (P.$$$ usesN) --| P.$$$ beginN))
   >> P.triple2;
 
 
 val new_header =
-  P.$$$ headerN |-- (P.!!! (P.text -- Scan.repeat P.semicolon -- P.$$$ theoryN |-- args)) ||
-  P.$$$ theoryN |-- P.!!! args;
+  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
+    (P.$$$ theoryN -- P.tags) |-- args)) ||
+  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
 
 val old_header =
   P.!!! (P.group "theory header"