diff -r bdf7d5f4d5b0 -r dd4297f5b495 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Sep 03 20:32:33 2008 +0000 +++ b/src/Pure/ROOT.ML Thu Sep 04 16:03:41 2008 +0200 @@ -22,6 +22,9 @@ cd "General"; use "ROOT.ML"; cd ".."; +(*concurrency within the ML runtime*) +use "Concurrent/schedule.ML"; + (*fundamental structures*) use "name.ML"; use "term.ML";