diff --git a/tools/afp_check_roots.scala b/tools/afp_check_roots.scala
--- a/tools/afp_check_roots.scala
+++ b/tools/afp_check_roots.scala
@@ -1,221 +1,209 @@
 /* Author: Lars Hupel and Fabian Huch, TU Muenchen
 
 Tools to check AFP session roots.
  */
 package afp
 
 
 import isabelle.{Path, *}
 
 import java.io.File as JFile
 
 
 object AFP_Check_Roots {
   val exclude = List("etc")
 
   def dir_entries(path: Path): List[String] =
     File.read_dir(path).filter(name => (path + Path.basic(name)).is_dir).filterNot(exclude.contains)
 
+  def root_sessions(root_file: Path): List[String] =
+    Sessions.parse_root(root_file).collect { case e: Sessions.Session_Entry => e.name }
+
 
   /* checks */
 
   case class Check[T](
     name: String,
     failure_msg: String,
     run: (Sessions.Structure, List[String], List[Path]) => List[T],
     failure_format: T => String = (t: T) => t.toString
   ) {
     override def toString: String = name
 
     def apply(
       structure: Sessions.Structure,
       sessions: List[String],
       check_dirs: List[Path],
       progress: Progress
     ): Boolean =
       run(structure, sessions, check_dirs) match {
         case Nil => true
         case offenders =>
           val msg = failure_msg + offenders.map("\n" + failure_format(_)).mkString
           progress.echo_error_message(msg)
           false
       }
   }
 
   val known_checks: List[Check[_]] =
     List(
       Check[String]("timeout",
         "The following entries contain sessions without timeouts or with timeouts not divisible by 300:",
         (structure, sessions, _) =>
-          sessions.flatMap { session_name =>
+          sessions.filter { session_name =>
             val info = structure(session_name)
             val timeout = info.options.real("timeout")
-            if (timeout == 0 || timeout % 300 != 0) Some(session_name) else None
+            timeout == 0 || timeout % 300 != 0
           }),
       Check[String]("chapter", "The following entries are not in the AFP chapter:",
-        (structure, sessions, _) =>
-          sessions.flatMap { session_name =>
-            val info = structure(session_name)
-            if (info.chapter != "AFP") Some(session_name) else None
-          }),
+        (structure, sessions, _) => sessions.filterNot(structure(_).chapter == "AFP")),
       Check[(String, List[String])]("groups", "The following sessions have wrong groups:",
         (structure, sessions, _) =>
           sessions.flatMap { session_name =>
             val info = structure(session_name)
             if (!info.groups.toSet.subsetOf(AFP.groups.keySet + "AFP") ||
               !info.groups.contains("AFP"))
               Some((session_name, info.groups))
             else None
           },
         t => t._1 + "{" + t._2.mkString(", ") + "}"),
       Check[String]("presence",
         "The following entries do not contain a corresponding session on top level:",
-        (structure, sessions, check_dirs) => {
-          val entries = check_dirs.flatMap(dir_entries)
-
-          entries.flatMap { entry_name =>
+        (structure, sessions, check_dirs) =>
+          check_dirs.flatMap(dir_entries).flatMap { entry_name =>
             if (!sessions.contains(entry_name) ||
               structure(entry_name).dir.base.implode != entry_name)
               Some(entry_name)
             else None
-          }
-        }),
+          }),
       Check[String]("roots",
         "The following entries do not match with the ROOTS file:",
-        (_, _, check_dirs) => {
+        (_, _, check_dirs) =>
           check_dirs.flatMap { dir =>
             val root_entries = Sessions.parse_roots(dir + Path.basic("ROOTS")).toSet
             val file_entries = dir_entries(dir).toSet
             (root_entries.union(file_entries) -- root_entries.intersect(file_entries)).toList
-          }
-        }
-      ),
+          }),
       Check[(String, List[Path])]("unused_thys",
         "The following sessions contain unused theories:",
         (structure, sessions, check_dirs) => {
           val selection = Sessions.Selection(sessions = sessions)
           val deps = structure.selection_deps(selection = selection)
 
           def is_thy_file(file: JFile): Boolean = file.isFile && file.getName.endsWith(".thy")
 
-          val entry_dirs = check_dirs.flatMap(dir => dir_entries(dir).map(dir + Path.basic(_)))
-          entry_dirs.flatMap { dir =>
-            val entry = dir.base.implode
+          check_dirs.flatMap(dir => dir_entries(dir).map(dir + Path.basic(_))).flatMap { dir =>
+            val sessions = root_sessions(dir + Path.basic("ROOT"))
+
             def rel_path(path: Path): Path = File.relative_path(dir.absolute, path.absolute).get
 
-            val sessions = Sessions.parse_root(dir + Path.basic("ROOT")).collect {
-              case e: Sessions.Session_Entry => e.name
-            }
             val theory_nodes = sessions.flatMap(deps.base_info(_).base.proper_session_theories)
             val thy_files = theory_nodes.map(node => rel_path(node.path))
 
-            val physical_files = File.find_files(dir.file, is_thy_file, include_dirs = true)
-            val rel_files = physical_files.map(file => rel_path(Path.explode(file.getAbsolutePath)))
+            val physical_files =
+              for (file <- File.find_files(dir.file, is_thy_file, include_dirs = true))
+              yield rel_path(Path.explode(file.getAbsolutePath))
 
-            val unused = rel_files.toSet -- thy_files.toSet
-            if (unused.nonEmpty) Some(entry -> unused.toList)
+            val unused = physical_files.toSet -- thy_files.toSet
+            if (unused.nonEmpty) Some(dir.base.implode -> unused.toList)
             else None
           }
         },
         t => t._1 + ": {" + t._2.mkString(", ") + "}"),
       Check[(String, List[Path])]("unused_document_files",
         "The following entries contain unused document files:",
         (structure, _, check_dirs) => {
-          val entry_dirs = check_dirs.flatMap(dir => dir_entries(dir).map(dir + Path.basic(_)))
-          entry_dirs.flatMap { dir =>
-            val entry = dir.base.implode
-
-            def rel_path(path: Path): Path = File.relative_path(dir.absolute, path.absolute).get
-
-            val sessions = Sessions.parse_root(dir + Path.basic("ROOT")).collect {
-              case e: Sessions.Session_Entry => e.name
-            }
+          check_dirs.flatMap(dir => dir_entries(dir).map(dir + Path.basic(_))).flatMap { dir =>
+            val sessions = root_sessions(dir + Path.basic("ROOT"))
 
             val session_document_files =
               sessions.flatMap { session_name =>
                 val info = structure(session_name)
                 info.document_files.map { case (dir, file) => (info.dir + dir, file) }
               }
 
+            def rel_path(path: Path): Path = File.relative_path(dir.absolute, path.absolute).get
+
             val document_files =
               session_document_files.map { case (dir, path) => rel_path(dir + path) }
 
-            val document_dirs = session_document_files.map(_._1.file).distinct
             val physical_files =
-              document_dirs.flatMap(File.find_files(_, _.isFile, include_dirs = true))
-            val rel_files = physical_files.map(file => rel_path(Path.explode(file.getAbsolutePath)))
+              for {
+                document_dir <- session_document_files.map(_._1.file).distinct
+                document_file <- File.find_files(document_dir, _.isFile, include_dirs = true)
+              } yield rel_path(Path.explode(document_file.getAbsolutePath))
 
-            val unused = rel_files.toSet -- document_files.toSet
-            if (unused.nonEmpty) Some(entry -> unused.toList) else None
+            val unused = physical_files.toSet -- document_files.toSet
+            if (unused.nonEmpty) Some(dir.base.implode -> unused.toList) else None
           }
         },
         t => t._1 + ": {" + t._2.mkString(", ") + "}"),
       Check[String]("document_presence",
         "The following entries do not contain a document root.tex",
         (structure, _, check_dirs) =>
           check_dirs.flatMap(dir_entries).filterNot(
             structure(_).document_files.map(_._2).contains(Path.basic("root.tex"))))
     ).sortBy(_.name)
 
   def the_check(name: String): Check[_] =
     known_checks.find(check => check.name == name) getOrElse
       error("Unkown check " + quote(name))
 
 
   /* check */
 
   def afp_check_roots(
     checks: List[Check[_]],
     dirs: List[Path],
     check_dirs: List[Path],
     progress: Progress = new Progress()
   ): Unit = {
     val structure = Sessions.load_structure(Options.init(), dirs = dirs, select_dirs = check_dirs)
     val sessions = structure.build_selection(Sessions.Selection.empty).sorted
 
     val bad = checks.exists(check => !check(structure, sessions, check_dirs, progress))
 
     if (bad) System.exit(1)
     else {
       progress.echo(sessions.length.toString + " sessions have been checked")
       progress.echo(checks.length.toString + " checks have found no errors")
     }
   }
 
 
   /* isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("afp_check_roots", "check ROOT files of AFP sessions",
     Scala_Project.here,
     { args =>
       var dirs: List[Path] = Nil
       var checks: List[Check[_]] = known_checks
       var check_dirs: List[Path] = Nil
 
       val getopts = Getopts("""
 Usage: isabelle afp_check_roots [OPTIONS]
 
   Options are:
     -d DIR      add entry dir
     -C NAMES    checks (default: """ + known_checks.mkString("\"", ",", "\"") + """)
     -D DIR      add and check entry dir
 
   Check ROOT files of AFP sessions.
 """,
       "d:" -> (arg => dirs ::= Path.explode(arg)),
       "C:" -> (arg => checks = Library.distinct(space_explode(',', arg)).map(the_check)),
       "D:" -> (arg => check_dirs ::= Path.explode(arg)))
 
       getopts(args)
 
       val progress = new Console_Progress()
 
       if (check_dirs.isEmpty) {
         check_dirs ::= AFP_Structure().thys_dir
       } else {
         dirs ::= AFP_Structure().thys_dir
       }
 
       afp_check_roots(checks, dirs, check_dirs, progress)
     })
 }