diff -r 961285f581e6 -r 687c822ee5e3 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -33,7 +33,7 @@
       else {
         val selection = Sessions.Selection(sessions = List(logic_name))
         val selected_sessions =
-          sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
+          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
         selected_sessions.build_requirements(List(logic_name)).
           map(a => File.platform_path(store.heap(a)))
       }