clarified signature: global_theories is always required;

--- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:03:57 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 17:15:49 2017 +0100
@@ -171,12 +171,12 @@
   }
 
   def deps(sessions: T,
+      global_theories: Map[String, String],
       progress: Progress = No_Progress,
       inlined_files: Boolean = false,
       verbose: Boolean = false,
       list_files: Boolean = false,
-      check_keywords: Set[String] = Set.empty,
-      global_theories: Map[String, String] = Map.empty): Deps =
+      check_keywords: Set[String] = Set.empty): Deps =
   {
     var cache_sources = Map.empty[JFile, SHA1.Digest]
     def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
@@ -330,8 +330,7 @@
     val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
 
     val sessions: T = if (all_known) full_sessions else selected_sessions
-    val deps =
-      Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories)
+    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
     val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
     (deps.errors, base)
   }

--- a/src/Pure/Tools/build.scala	Tue Oct 31 17:03:57 2017 +0100
+++ b/src/Pure/Tools/build.scala	Tue Oct 31 17:15:49 2017 +0100
@@ -398,9 +398,9 @@
               exclude_sessions, session_groups, sessions) ++ selection)
 
       val deps0 =
-        Sessions.deps(selected_sessions0, progress = progress, inlined_files = true,
-          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
-          global_theories = full_sessions.global_theories).check_errors
+        Sessions.deps(selected_sessions0, full_sessions.global_theories,
+          progress = progress, inlined_files = true, verbose = verbose,
+          list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
         val outdated =
@@ -417,8 +417,8 @@
         val (selected, selected_sessions) =
           full_sessions.selection(Sessions.Selection(sessions = outdated))
         val deps =
-          Sessions.deps(selected_sessions, inlined_files = true,
-            global_theories = full_sessions.global_theories).check_errors
+          Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
+            .check_errors
         (selected, selected_sessions, deps)
       }
       else (selected0, selected_sessions0, deps0)

--- a/src/Pure/Tools/imports.scala	Tue Oct 31 17:03:57 2017 +0100
+++ b/src/Pure/Tools/imports.scala	Tue Oct 31 17:15:49 2017 +0100
@@ -103,8 +103,8 @@
     val (selected, selected_sessions) = full_sessions.selection(selection)
 
     val deps =
-      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
-        global_theories = full_sessions.global_theories).check_errors
+      Sessions.deps(selected_sessions, full_sessions.global_theories,
+        progress = progress, verbose = verbose).check_errors
 
     val root_keywords = Sessions.root_syntax.keywords