# HG changeset patch
# User wenzelm
# Date 1507381074 -7200
# Node ID 8df01b0db3e96ba1ba08b16e67d8796e9bf66616
# Parent  f90a1370cb6a10087a365c1cc71895665a11dad6# Parent  b74b9d0bf7633374bfa5d65d5b75f0258ca9d1d7
merged

diff -r f90a1370cb6a -r 8df01b0db3e9 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 07 14:56:30 2017 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 07 14:57:54 2017 +0200
@@ -18,9 +18,7 @@
 
   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
 
-  def merge(syns: List[Outer_Syntax]): Outer_Syntax =
-    if (syns.isEmpty) Thy_Header.bootstrap_syntax
-    else (syns.head /: syns.tail)(_ ++ _)
+  def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
 
 
   /* string literals */
@@ -109,6 +107,7 @@
 
   def ++ (other: Outer_Syntax): Outer_Syntax =
     if (this eq other) this
+    else if (this eq Outer_Syntax.empty) other
     else {
       val keywords1 = keywords ++ other.keywords
       val completion1 = completion ++ other.completion
diff -r f90a1370cb6a -r 8df01b0db3e9 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Sat Oct 07 14:56:30 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Sat Oct 07 14:57:54 2017 +0200
@@ -49,14 +49,14 @@
         val name = entry.name.theory
         val imports = entry.header.imports.map(p => p._1.theory)
 
-        if (graph.defined(name))
-          error("Duplicate loaded theory entry " + quote(name))
+        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
+        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
 
-        for (dep <- imports if !graph.defined(dep))
-          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
+        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
+        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
+        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
 
-        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
-        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
+        graph2.map_node(name, _ => syntax)
       })
 
     def loaded_files: List[(String, List[Path])] =