# 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 =