src/Pure/ML/ml_statistics.ML

   PolyML.Statistics.setUserCounter (7, workers_waiting));
 
 
 (* get properties *)
 
+local
+
 fun make_properties
    {gcFullGCs,
     gcPartialGCs,
     gcSharePasses,
     sizeAllocation,

     timeGCSystem,
     timeGCUser,
     timeNonGCReal,
     timeNonGCSystem,
     timeNonGCUser,
-    userCounters} =
+    userCounters, ...} =
   let
     val tasks_ready = Vector.sub (userCounters, 0);
     val tasks_pending = Vector.sub (userCounters, 1);
     val tasks_running = Vector.sub (userCounters, 2);
     val tasks_passive = Vector.sub (userCounters, 3);

      ("time_elapsed_GC", print_real (Time.toReal timeGCReal)),
      ("time_CPU", print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
      ("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 *)
 
 fun monitor pid delay =