--- a/src/Pure/ROOT Sat Apr 02 20:23:51 2016 +0200
+++ b/src/Pure/ROOT Sat Apr 02 20:33:34 2016 +0200
@@ -112,6 +112,7 @@
"ML/ml_name_space.ML"
"ML/ml_options.ML"
"ML/ml_pp.ML"
+ "ML/ml_pervasive.ML"
"ML/ml_pretty.ML"
"ML/ml_profiling.ML"
"ML/ml_statistics.ML"