changeset 62585 | 5d4ed917450d |
parent 62584 | 6cd36a0d2a28 |
child 62643 | 6f7ac44365d7 |
--- 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";