src/Pure/General/timing.scala

--- a/src/Pure/General/timing.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/timing.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -26,7 +26,7 @@
       val timing = stop - start
       if (timing.is_relevant) {
         val msg = if (message == null) null else message(result)
-        output((if (msg == null || msg == "") "" else msg + ": ") + timing.message + " elapsed time")
+        output(if_proper(msg, msg + ": ") + timing.message + " elapsed time")
       }
 
       Exn.release(result)