src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/Pure/ROOT.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -64,6 +64,7 @@
 
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
+use "PIDE/sendback.ML";
 
 use "General/graph.ML";