# HG changeset patch
# User wenzelm
# Date 1605008936 -3600
# Node ID ab4a0b19648adeb7ae6b9fe503b74f08a19e82d6
# Parent  79661d12155ef0506e4f13d246b523f327da6ff4
tuned signature;

diff -r 79661d12155e -r ab4a0b19648a src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Nov 10 12:45:20 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Nov 10 12:48:56 2020 +0100
@@ -32,7 +32,7 @@
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
-        sessions_structure.selection(Sessions.Selection.session(logic_name)).
+        sessions_structure.selection(logic_name).
           build_requirements(List(logic_name)).
           map(a => File.platform_path(store.the_heap(a)))
       }
diff -r 79661d12155e -r ab4a0b19648a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 10 12:45:20 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 10 12:48:56 2020 +0100
@@ -711,6 +711,8 @@
         restrict(build_graph), restrict(imports_graph))
     }
 
+    def selection(session: String): Structure = selection(Selection.session(session))
+
     def selection_deps(
       options: Options,
       selection: Selection,