more integrity checks of theory names vs. full node names;

--- a/src/Pure/General/multi_map.scala	Fri Feb 14 11:10:28 2014 +0100
+++ b/src/Pure/General/multi_map.scala	Fri Feb 14 14:39:44 2014 +0100
@@ -25,6 +25,8 @@
 {
   /* Multi_Map operations */
 
+  def iterator_list: Iterator[(A, List[B])] = rep.iterator
+
   def get_list(a: A): List[B] = rep.getOrElse(a, Nil)
 
   def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =

--- a/src/Pure/Thy/thy_info.ML	Fri Feb 14 11:10:28 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Feb 14 14:39:44 2014 +0100
@@ -324,8 +324,8 @@
           else
             error (loader_msg "incoherent imports for theory" [name] ^
               Position.here require_pos ^ ":\n" ^
-              Path.print node_name ^ " versus\n" ^
-              Path.print node_name')
+              "  " ^ Path.print node_name ^ "\n" ^
+              "  " ^ Path.print node_name')
       | check_entry _ = ();
   in
     (case try (String_Graph.get_node tasks) name of

--- a/src/Pure/Thy/thy_info.scala	Fri Feb 14 11:10:28 2014 +0100
+++ b/src/Pure/Thy/thy_info.scala	Fri Feb 14 14:39:44 2014 +0100
@@ -42,23 +42,45 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Nil, Set.empty)
+    val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty)
   }
 
   final class Dependencies private(
     rev_deps: List[Dep],
     val keywords: Thy_Header.Keywords,
-    val seen: Set[Document.Node.Name])
+    val seen_names: Multi_Map[String, Document.Node.Name],
+    val seen_positions: Multi_Map[String, Position.T])
   {
     def :: (dep: Dep): Dependencies =
-      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, seen)
+      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
+        seen_names, seen_positions)
 
-    def + (name: Document.Node.Name): Dependencies =
-      new Dependencies(rev_deps, keywords, seen = seen + name)
+    def + (thy: (Document.Node.Name, Position.T)): Dependencies =
+    {
+      val (name, pos) = thy
+      new Dependencies(rev_deps, keywords,
+        seen_names + (name.theory -> name),
+        seen_positions + (name.theory -> pos))
+    }
 
     def deps: List[Dep] = rev_deps.reverse
 
-    def errors: List[String] = deps.flatMap(dep => dep.header.errors)
+    def errors: List[String] =
+    {
+      val header_errors = deps.flatMap(dep => dep.header.errors)
+      val import_errors =
+        (for {
+          (theory, names) <- seen_names.iterator_list
+          if !thy_load.loaded_theories(theory)
+          if names.length > 1
+        } yield
+          "Incoherent imports for theory " + quote(theory) + ":\n" +
+            cat_lines(names.flatMap(name =>
+              seen_positions.get_list(theory).map(pos =>
+                "  " + quote(name.node) + Position.here(pos))))
+        ).toList
+      header_errors ::: import_errors
+    }
 
     lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
 
@@ -79,32 +101,38 @@
   }
 
   private def require_thys(initiators: List[Document.Node.Name],
-      required: Dependencies, names: List[Document.Node.Name]): Dependencies =
-    (required /: names)(require_thy(initiators, _, _))
+      required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    (required /: thys)(require_thy(initiators, _, _))
 
   private def require_thy(initiators: List[Document.Node.Name],
-      required: Dependencies, name: Document.Node.Name): Dependencies =
+      required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
   {
-    if (required.seen(name)) required
-    else if (thy_load.loaded_theories(name.theory)) required + name
+    val (name, require_pos) = thy
+    val theory = name.theory
+
+    def message: String =
+      "The error(s) above occurred for theory " + quote(theory) +
+        required_by(initiators) + Position.here(require_pos)
+
+    val required1 = required + thy
+    if (required.seen_names.isDefinedAt(theory) || thy_load.loaded_theories(theory))
+      required1
     else {
-      def message: String =
-        "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators)
-
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val header =
           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)
+        val imports = header.imports.map((_, Position.File(name.node)))
+        Dep(name, header) :: require_thys(name :: initiators, required1, imports)
       }
       catch {
         case e: Throwable =>
-          Dep(name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
+          Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
       }
     }
   }
 
-  def dependencies(names: List[Document.Node.Name]): Dependencies =
-    require_thys(Nil, Dependencies.empty, names)
+  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    require_thys(Nil, Dependencies.empty, thys)
 }

--- a/src/Pure/Tools/build.scala	Fri Feb 14 11:10:28 2014 +0100
+++ b/src/Pure/Tools/build.scala	Fri Feb 14 14:39:44 2014 +0100
@@ -432,7 +432,7 @@
             val thy_deps =
               thy_info.dependencies(
                 info.theories.map(_._2).flatten.
-                  map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
+                  map(thy => (thy_load.node_name(info.dir + Thy_Load.thy_path(thy)), info.pos)))
 
             thy_deps.errors match {
               case Nil =>