diff -r b9c716a9fb5f -r 1498f0362362 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Sat Feb 16 02:08:07 2008 +0100
+++ b/src/Pure/General/ROOT.ML	Sat Feb 16 16:43:53 2008 +0100
@@ -32,4 +32,5 @@
 use "buffer.ML";
 use "history.ML";
 use "xml.ML";
+use "system_process.ML";