proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
(* Title: Pure/ML/ml_statistics_dummy.ML
Author: Makarius
ML runtime statistics -- dummy version.
*)
signature ML_STATISTICS =
sig
val get: unit -> Properties.T
end;
structure ML_Statistics: ML_STATISTICS =
struct
fun get () = [];
end;