# HG changeset patch
# User wenzelm
# Date 1357403067 -3600
# Node ID d5725e56cd049b5f98e0948555e03c0d646126ea
# Parent  f310d1735d935246a8f819222929c21e66e0bb0e
more direct property names;

diff -r f310d1735d93 -r d5725e56cd04 src/Pure/ML/ml_statistics_polyml-5.5.0.ML
--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Sat Jan 05 16:16:22 2013 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Sat Jan 05 17:24:27 2013 +0100
@@ -35,7 +35,7 @@
       userCounters} = PolyML.Statistics.getLocalStats ();
     val user_counters =
       Vector.foldri
-        (fn (i, j, res) => ("user_counter" ^ Markup.print_int (i + 1), Markup.print_int j) :: res)
+        (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
         [] userCounters;
   in
     [("full_GCs", Markup.print_int gcFullGCs),