diff -r 6cd36a0d2a28 -r 5d4ed917450d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 10 09:50:53 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 10 09:56:29 2016 +0100
@@ -107,8 +107,8 @@
 
 use "Concurrent/synchronized.ML";
 use "Concurrent/counter.ML";
-use "Concurrent/random.ML";
 
+use "General/random.ML";
 use "General/properties.ML";
 use "General/output.ML";
 use "PIDE/markup.ML";