# HG changeset patch
# User wenzelm
# Date 1570364278 -7200
# Node ID b254a95b6e771a2cd7e777b2122b4d4df8bf8635
# Parent  15656ad28691822aad11de60d52570f936c87eba
tuned signature;

diff -r 15656ad28691 -r b254a95b6e77 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Oct 05 15:34:54 2019 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun Oct 06 14:17:58 2019 +0200
@@ -35,8 +35,7 @@
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
-        val selection = Sessions.Selection(sessions = List(logic_name))
-        sessions_structure1.selection(selection).
+        sessions_structure1.selection(Sessions.Selection.session(logic_name)).
           build_requirements(List(logic_name)).
           map(a => File.platform_path(_store.the_heap(a)))
       }
diff -r 15656ad28691 -r b254a95b6e77 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Oct 05 15:34:54 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun Oct 06 14:17:58 2019 +0200
@@ -547,6 +547,7 @@
   {
     val empty: Selection = Selection()
     val all: Selection = Selection(all_sessions = true)
+    def session(session: String): Selection = Selection(sessions = List(session))
   }
 
   sealed case class Selection(