diff -r 98fe7a10ace3 -r a4d7da18ac5c src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Nov 26 20:49:40 2020 +0000
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 26 23:23:19 2020 +0100
@@ -265,12 +265,19 @@
 
       val result =
       {
+        val theory_timing =
+          theory_timings.iterator.map(
+            { case props @ Markup.Name(name) => name -> props }).toMap
+        val used_theory_timings =
+          for { (name, _) <- deps(session_name).used_theories }
+            yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
+
         val more_output =
           Library.trim_line(stdout.toString) ::
             messages.toList.map(message =>
               Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
-            theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
+            used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::