# HG changeset patch
# User wenzelm
# Date 1507373405 -7200
# Node ID e8f27a35ee0fda8f2896397658bbfed10e4765f6
# Parent  0cd29455a5e8f8f66a4f26b2ff673256e9fcc9b6
permissive loaded_theories (amending 67dbf5cdc056): user errors are produced e.g. in Known.make;

diff -r 0cd29455a5e8 -r e8f27a35ee0f src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Oct 06 21:33:33 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Sat Oct 07 12:50:05 2017 +0200
@@ -49,14 +49,13 @@
         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(_, Thy_Header.bootstrap_syntax))
+        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 syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
-        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
+        val syntax =
+          Outer_Syntax.merge((name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))) +
+            entry.header
+        graph2.map_node(name, _ => syntax)
       })
 
     def loaded_files: List[(String, List[Path])] =