src/Pure/ML/ml_statistics_dummy.ML

--- a/src/Pure/ML/ml_statistics_dummy.ML	Sat Mar 05 13:51:21 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  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;
-