# HG changeset patch
# User wenzelm
# Date 1571313974 -7200
# Node ID 15ad4c045590982f48709ca54d3f03f7222aebfe
# Parent  62b3acc801ece9234bad2da6fc3c618c519b10a5
more robust;

diff -r 62b3acc801ec -r 15ad4c045590 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Oct 16 21:55:17 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu Oct 17 14:06:14 2019 +0200
@@ -48,17 +48,21 @@
             for (theory <- Export.read_theory_names(db, session))
             yield {
               progress.echo("Reading theory " + theory)
-              read_theory(Export.Provider.database(db, session, theory),
-                session, theory, types = types, consts = consts,
-                axioms = axioms, thms = thms, classes = classes, locales = locales,
-                locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
-                typedefs = typedefs, cache = Some(cache))
+              if (theory == Thy_Header.PURE) read_pure_theory(store, cache = Some(cache))
+              else {
+                read_theory(Export.Provider.database(db, session, theory),
+                  session, theory, types = types, consts = consts,
+                  axioms = axioms, thms = thms, classes = classes, locales = locales,
+                  locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
+                  typedefs = typedefs, cache = Some(cache))
+              }
             }
           }
         }))
 
     val graph0 =
-      (Graph.string[Option[Theory]] /: thys) { case (g, thy) => g.new_node(thy.name, Some(thy)) }
+      (Graph.string[Option[Theory]] /: thys) {
+        case (g, thy) => g.default_node(thy.name, Some(thy)) }
     val graph1 =
       (graph0 /: thys) { case (g0, thy) =>
         (g0 /: thy.parents) { case (g1, parent) =>