src/Pure/Tools/build.ML
changeset 51220 e140c8fa485a
parent 51218 6425a0d3b7ac
child 51228 dff3471dd8bc
     1.1 --- a/src/Pure/Tools/build.ML	Tue Feb 19 14:47:57 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Tue Feb 19 16:49:40 2013 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4  
     1.5  fun build args_file = Command_Line.tool (fn () =>
     1.6      let
     1.7 -      val (timings, (do_output, (options, (verbose, (browser_info,
     1.8 +      val (command_timings, (do_output, (options, (verbose, (browser_info,
     1.9            (parent_name, (name, theories))))))) =
    1.10          File.read (Path.explode args_file) |> YXML.parse_body |>
    1.11            let open XML.Decode in
    1.12 @@ -126,7 +126,7 @@
    1.13  
    1.14        val last_timing =
    1.15          the_default Timing.zero o
    1.16 -          Timings.lookup (make_timings timings) o Toplevel.approximative_id;
    1.17 +          Timings.lookup (make_timings command_timings) o Toplevel.approximative_id;
    1.18  
    1.19        val res1 =
    1.20          theories |>