diff -r bc85d93aad23 -r 7b112eedc859 src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Wed Jul 15 17:10:26 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Wed Jul 15 20:06:45 2020 +0200
@@ -50,6 +50,8 @@
 
 (* get properties *)
 
+local
+
 fun make_properties
    {gcFullGCs,
     gcPartialGCs,
@@ -73,7 +75,7 @@
     timeNonGCReal,
     timeNonGCSystem,
     timeNonGCUser,
-    userCounters} =
+    userCounters, ...} =
   let
     val tasks_ready = Vector.sub (userCounters, 0);
     val tasks_pending = Vector.sub (userCounters, 1);
@@ -117,12 +119,16 @@
      ("time_GC", print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))]
   end;
 
+in
+
 fun get () =
   make_properties (PolyML.Statistics.getLocalStats ());
 
 fun get_external pid =
   make_properties (PolyML.Statistics.getRemoteStats pid);
 
+end;
+
 
 (* monitor process *)