diff -r ce523820ff75 -r 3414557c2dda src/Pure/mk
--- a/src/Pure/mk	Thu Dec 01 18:41:44 2005 +0100
+++ b/src/Pure/mk	Thu Dec 01 18:41:46 2005 +0100
@@ -81,7 +81,7 @@
 
 # run isabelle
 
-SECONDS=0
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 if [ -z "$RAW" ]; then
   ITEM="Pure"
@@ -107,13 +107,13 @@
   RC="$?"
 fi
 
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
 
 
 # exit status
 
 if [ "$RC" -eq 0 ]; then
-  echo "Finished $ITEM ($ELAPSED elapsed time)"
+  echo "Finished $ITEM ($TIMES_REPORT)"
   gzip --force "$LOG"
 else
   echo "$ITEM FAILED"