# HG changeset patch
# User wenzelm
# Date 1261514801 -3600
# Node ID 0a5e2c5195d5703d6e0246c602e8e578aca8ac6a
# Parent  446a33b874b3ceaba1e14c177d5f6da5333e005f
tuned;

diff -r 446a33b874b3 -r 0a5e2c5195d5 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Dec 22 19:38:06 2009 +0100
+++ b/src/Pure/Thy/thy_header.ML	Tue Dec 22 21:46:41 2009 +0100
@@ -35,7 +35,7 @@
 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 file = P.$$$ "(" |-- P.!!! (file_name --| P.$$$ ")") >> rpair false || file_name >> rpair true;
 val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
 
 val args =