--- 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";