| 50255 |      1 | (*  Title:      Pure/ML/ml_statistics_dummy.ML
 | 
|  |      2 |     Author:     Makarius
 | 
|  |      3 | 
 | 
|  |      4 | ML runtime statistics -- dummy version.
 | 
|  |      5 | *)
 | 
|  |      6 | 
 | 
|  |      7 | signature ML_STATISTICS =
 | 
|  |      8 | sig
 | 
|  |      9 |   val get: unit -> Properties.T
 | 
|  |     10 | end;
 | 
|  |     11 | 
 | 
|  |     12 | structure ML_Statistics: ML_STATISTICS =
 | 
|  |     13 | struct
 | 
|  |     14 | 
 | 
|  |     15 | fun get () = [];
 | 
|  |     16 | 
 | 
|  |     17 | end;
 | 
|  |     18 | 
 |