src/Pure/ROOT.ML
changeset 28120 dd4297f5b495
parent 27642 c0db1220b071
child 28134 1179b32f885d
--- 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";