diff -r 6cd36a0d2a28 -r 5d4ed917450d src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Mar 10 09:50:53 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 10 09:56:29 2016 +0100
@@ -12,7 +12,6 @@
     "Concurrent/multithreading.ML"
     "Concurrent/par_exn.ML"
     "Concurrent/par_list.ML"
-    "Concurrent/random.ML"
     "Concurrent/single_assignment.ML"
     "Concurrent/standard_thread.ML"
     "Concurrent/synchronized.ML"
@@ -45,6 +44,7 @@
     "General/print_mode.ML"
     "General/properties.ML"
     "General/queue.ML"
+    "General/random.ML"
     "General/same.ML"
     "General/scan.ML"
     "General/secure.ML"