diff -r 26fa2e8761fb -r 215db9299a1a src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sun Feb 18 15:16:20 2024 +0100 +++ b/src/Pure/ML/ml_process.scala Sun Feb 18 19:09:05 2024 +0100 @@ -24,7 +24,7 @@ session_background.sessions_structure.selection(logic_name). build_requirements(List(logic_name)). - map(store.the_heap) + map(name => store.get_session(name).the_heap) } def apply(