--- a/src/Pure/Tools/build.ML Tue Apr 09 21:14:00 2013 +0200
+++ b/src/Pure/Tools/build.ML Tue Apr 09 21:22:15 2013 +0200
@@ -21,7 +21,8 @@
fun update_timings props =
(case Markup.parse_command_timing_properties props of
SOME ({file, offset, name}, time) =>
- Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
+ Symtab.map_default (file, Inttab.empty)
+ (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, Time.+ (t, time))))
| NONE => I);
fun approximative_id name pos =