diff -r e17a1f179bb0 -r 0d60de55c58a src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Dec 07 13:38:32 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala	Fri Dec 07 13:56:01 2012 +0100
@@ -84,16 +84,20 @@
         val future_header: JFuture[Exn.Result[Document.Node.Header]] =
           if (files) {
             val string = thy_load.with_thy_text(name, _.toString)
-            default_thread_pool.submit(() =>
-              Exn.capture {
-                try {
-                  val syntax0 = syntax.add_keywords(header0.keywords)
-                  val files = thy_load.theory_body_files(syntax0, string)
-                  header0.copy(uses = header0.uses ::: files.map((_, false)))
+            val syntax0 = syntax.add_keywords(header0.keywords)
+
+            if (thy_load.body_files_test(syntax0, string)) {
+              default_thread_pool.submit(() =>
+                Exn.capture {
+                  try {
+                    val files = thy_load.body_files(syntax0, string)
+                    header0.copy(uses = header0.uses ::: files.map((_, false)))
+                  }
+                  catch { case ERROR(msg) => err(msg) }
                 }
-                catch { case ERROR(msg) => err(msg) }
-              }
-            )
+              )
+            }
+            else Library.future_value(Exn.Res(header0))
           }
           else Library.future_value(Exn.Res(header0))