src/Pure/Thy/thy_info.scala

--- a/src/Pure/Thy/thy_info.scala	Thu Nov 21 17:45:37 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala	Thu Nov 21 17:50:23 2013 +0100
@@ -58,6 +58,8 @@
 
     def deps: List[Dep] = rev_deps.reverse
 
+    def errors: List[String] = deps.flatMap(dep => dep.header.errors)
+
     lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
 
     def loaded_theories: Set[String] =
@@ -86,15 +88,15 @@
     if (required.seen(name)) required
     else if (thy_load.loaded_theories(name.theory)) required + name
     else {
-      def err(msg: String): Nothing =
-        cat_error(msg, "The error(s) above occurred while examining theory " +
-          quote(name.theory) + required_by(initiators))
+      def message: String =
+        "The error(s) above occurred while examining theory " +
+          quote(name.theory) + required_by(initiators)
 
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val header =
-          try { thy_load.check_thy(name) }
-          catch { case ERROR(msg) => err(msg) }
+          try { thy_load.check_thy(name).cat_errors(message) }
+          catch { case ERROR(msg) => cat_error(msg, message) }
         Dep(name, header) :: require_thys(name :: initiators, required + name, header.imports)
       }
       catch {