diff -r d96cb03caf9e -r d2bb4b5ed862 src/Pure/Thy/thy_header.ML
--- 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));