src/Pure/ROOT.ML
changeset 62585 5d4ed917450d
parent 62584 6cd36a0d2a28
child 62643 6f7ac44365d7
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 10 09:50:53 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 10 09:56:29 2016 +0100
     1.3 @@ -107,8 +107,8 @@
     1.4  
     1.5  use "Concurrent/synchronized.ML";
     1.6  use "Concurrent/counter.ML";
     1.7 -use "Concurrent/random.ML";
     1.8  
     1.9 +use "General/random.ML";
    1.10  use "General/properties.ML";
    1.11  use "General/output.ML";
    1.12  use "PIDE/markup.ML";