# HG changeset patch
# User wenzelm
# Date 1491564467 -7200
# Node ID 741d40f42dd3fbebc9d3b52ad6e396a020cb3f3f
# Parent  4527b33d5b3e748ecea29ec4253646ba28ffd87f
more checks;

diff -r 4527b33d5b3e -r 741d40f42dd3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 07 13:19:11 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 13:27:47 2017 +0200
@@ -290,10 +290,16 @@
       if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
 
     def global_theories: Set[String] =
-      (for {
-        (_, (info, _)) <- imports_graph.iterator
-        name <- info.global_theories.iterator }
-       yield name).toSet
+      (Set.empty[String] /:
+        (for {
+          (_, (info, _)) <- imports_graph.iterator
+          thy <- info.global_theories.iterator }
+         yield (thy, info.pos)))(
+          { case (set, (thy, pos)) =>
+             if (set.contains(thy))
+               error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
+             else set + thy
+           })
 
     def selection(select: Selection): (List[String], T) =
     {