src/Pure/Tools/dump.scala

     if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
       system_mode = system_mode) != 0) error(logic + " FAILED")
 
     val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
 
+
+    /* dependencies */
+
     val deps =
       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
         selection_deps(selection)
 
+    val include_sessions =
+      deps.sessions_structure.imports_topological_order
+
+    val use_theories =
+      deps.sessions_structure.build_topological_order.
+        flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
+
+
+    /* session */
+
     val session =
       Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
-        include_sessions = deps.sessions_structure.imports_topological_order,
-        progress = progress, log = log)
+        include_sessions = include_sessions, progress = progress, log = log)
 
-    val theories = deps.all_known.theory_graph.topological_order.map(_.theory)
-    val theories_result = session.use_theories(theories, progress = progress)
-
-    val args = Aspect_Args(dump_options, progress, output_dir, theories_result)
-
-    try { aspects.foreach(aspect => aspect.operation(args)) }
+    try {
+      val theories_result = session.use_theories(use_theories, progress = progress)
+      val args = Aspect_Args(dump_options, progress, output_dir, theories_result)
+      aspects.foreach(_.operation(args))
+    }
     catch { case exn: Throwable => session.stop (); throw exn }
     session.stop()
   }