1.1 --- a/src/Pure/System/session.ML	Tue Jan 22 11:28:54 2013 +0100
     1.2 +++ b/src/Pure/System/session.ML	Thu Jan 24 17:18:13 2013 +0100
     1.3 @@ -96,9 +96,9 @@
     1.4      val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
     1.5        |> Real.fmt (StringCvt.FIX (SOME 2));
     1.6  
     1.7 -    val _ =
     1.8 -      writeln ("\fTiming = " ^ ML_Syntax.print_properties
     1.9 -        ([("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]));
    1.10 +    val timing_props =
    1.11 +      [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
    1.12 +    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
    1.13      val _ =
    1.14        if verbose then
    1.15          Output.physical_stderr ("Timing " ^ name ^ " (" ^