changeset 48638 | 22d65e375c01 |
parent 46961 | 5c6955f487e5 |
child 48707 | ba531af91148 |
--- a/src/Pure/Thy/thy_header.ML Wed Aug 01 18:57:17 2012 +0200 +++ b/src/Pure/Thy/thy_header.ML Wed Aug 01 19:53:20 2012 +0200 @@ -97,7 +97,7 @@ val args = theory_name -- - (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) -- + Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] -- Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] -- Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --| Parse.$$$ beginN >>