present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
eliminated implicit state: these theories are globally unique;