--- a/src/Pure/ROOT Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ROOT Tue Mar 01 21:10:29 2016 +0100
@@ -28,6 +28,7 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
+ "RAW/secure.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -59,6 +60,7 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
+ "RAW/secure.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -105,7 +107,6 @@
"General/queue.ML"
"General/same.ML"
"General/scan.ML"
- "General/secure.ML"
"General/seq.ML"
"General/sha1.ML"
"General/sha1_polyml.ML"
@@ -166,7 +167,6 @@
"ML/ml_file.ML"
"ML/ml_lex.ML"
"ML/ml_options.ML"
- "ML/ml_parse.ML"
"ML/ml_statistics.ML"
"ML/ml_statistics_dummy.ML"
"ML/ml_syntax.ML"