# HG changeset patch
# User wenzelm
# Date 1551635108 -3600
# Node ID bb41977edb7e82ff4e19401a50552c612e355773
# Parent  60b924cda7649fb862425358bc4f3cee7560475d
tuned signature;

diff -r 60b924cda764 -r bb41977edb7e src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sun Mar 03 16:00:14 2019 +0100
+++ b/src/Pure/Tools/dump.scala	Sun Mar 03 18:45:08 2019 +0100
@@ -75,28 +75,22 @@
 
   /* dependencies */
 
-  def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress)
-    : List[Document.Node.Name] =
-  {
-    deps.used_theories_condition(options, progress.echo_warning).map(_._2)
-  }
-
   def dependencies(
     options: Options,
     progress: Progress = No_Progress,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
-    selection: Sessions.Selection = Sessions.Selection.empty)
-      : (Sessions.Deps, List[Document.Node.Name]) =
+    selection: Sessions.Selection = Sessions.Selection.empty): Sessions.Deps =
   {
-    val deps =
-      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
-        selection_deps(options, selection, progress = progress,
-          uniform_session = true, loading_sessions = true)
+    Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
+      selection_deps(options, selection, progress = progress,
+        uniform_session = true, loading_sessions = true)
+  }
 
-    val theories = used_theories(options, deps, progress = progress)
-
-    (deps, theories)
+  def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress)
+    : List[Document.Node.Name] =
+  {
+    deps.used_theories_condition(options, progress.echo_warning).map(_._2)
   }
 
 
@@ -218,7 +212,7 @@
 
     val deps =
       dependencies(dump_options, progress = progress,
-        dirs = dirs, select_dirs = select_dirs, selection = selection)._1
+        dirs = dirs, select_dirs = select_dirs, selection = selection)
 
     val resources =
       Headless.Resources.make(dump_options, logic, progress = progress, log = log,
diff -r 60b924cda764 -r bb41977edb7e src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sun Mar 03 16:00:14 2019 +0100
+++ b/src/Pure/Tools/update.scala	Sun Mar 03 18:45:08 2019 +0100
@@ -23,7 +23,7 @@
 
     val deps =
       Dump.dependencies(dump_options, progress = progress,
-        dirs = dirs, select_dirs = select_dirs, selection = selection)._1
+        dirs = dirs, select_dirs = select_dirs, selection = selection)
 
     val resources =
       Headless.Resources.make(dump_options, logic, progress = progress, log = log,