args: explicit groups for file_name, theory_name;

--- a/src/Pure/Thy/thy_header.ML	Fri Aug 15 15:51:04 2008 +0200
+++ b/src/Pure/Thy/thy_header.ML	Fri Aug 15 15:51:06 2008 +0200
@@ -33,11 +33,14 @@
 
 (* header args *)
 
-val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
+val file_name = P.group "file name" P.name;
+val theory_name = P.group "theory name" P.name;
+
+val file = (P.$$$ "(" |-- P.!!! (file_name --| P.$$$ ")")) >> rpair false || file_name >> rpair true;
 val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
 
 val args =
-  P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN))
+  theory_name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 theory_name -- uses --| P.$$$ beginN))
   >> P.triple2;