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