--- a/src/Pure/Thy/thy_header.ML Sat Mar 14 17:23:58 2015 +0100
+++ b/src/Pure/Thy/thy_header.ML Sat Mar 14 18:18:40 2015 +0100
@@ -103,8 +103,9 @@
local
-val imports =
- Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
+fun imports name =
+ if name = Context.PureN then Scan.succeed []
+ else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
val opt_files =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
@@ -128,7 +129,7 @@
val args =
Parse.position Parse.theory_name :|-- (fn (name, pos) =>
- (if name = Context.PureN then Scan.succeed [] else imports) --
+ imports name --
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));