src/Pure/ML/ml_process.scala
changeset 67025 961285f581e6
parent 66961 f855f9aed72f
child 67026 687c822ee5e3
--- a/src/Pure/ML/ml_process.scala	Tue Nov 07 15:50:36 2017 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Nov 07 16:44:25 2017 +0100
@@ -32,7 +32,7 @@
       if (raw_ml_system) Nil
       else {
         val selection = Sessions.Selection(sessions = List(logic_name))
-        val (_, selected_sessions) =
+        val selected_sessions =
           sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
         selected_sessions.build_requirements(List(logic_name)).
           map(a => File.platform_path(store.heap(a)))