diff -r b9214b89d994 -r 7ed337926ed8 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Feb 27 11:59:22 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 27 14:15:14 2023 +0100
@@ -492,8 +492,7 @@
   def session_finished(session_name: String, timing: Timing): String =
     "Finished " + session_name + " (" + timing.message_resources + ")"
 
-  def session_timing(session_name: String, build_log: Build_Log.Session_Info): String = {
-    val props = build_log.session_timing
+  def session_timing(session_name: String, props: Properties.T): String = {
     val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
     val timing = Markup.Timing_Properties.get(props)
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
@@ -585,7 +584,9 @@
     process_result.err_lines.foreach(progress.echo)
 
     if (process_result.ok) {
-      if (verbose) progress.echo(Build_Process.session_timing(session_name, build_log))
+      if (verbose) {
+        progress.echo(Build_Process.session_timing(session_name, build_log.session_timing))
+      }
       progress.echo(Build_Process.session_finished(session_name, process_result.timing))
     }
     else {