diff -r 693276dcc512 -r bed4b2738d8a src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Apr 04 14:00:47 2012 +0200 +++ b/src/Pure/ROOT.ML Wed Apr 04 14:19:47 2012 +0200 @@ -251,6 +251,7 @@ use "Thy/present.ML"; use "Thy/thy_load.ML"; use "Thy/thy_info.ML"; +use "PIDE/command.ML"; use "PIDE/document.ML"; use "Thy/rail.ML";