# HG changeset patch
# User wenzelm
# Date 1218808266 -7200
# Node ID 62ac62e30ab1bf95b045c2656584e88ac741e387
# Parent  c9e8a5bda32bd7e0a71874e2e678735f3f285f8b
args: explicit groups for file_name, theory_name;

diff -r c9e8a5bda32b -r 62ac62e30ab1 src/Pure/Thy/thy_header.ML
--- 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;