src/Pure/General/ROOT.ML

--- a/src/Pure/General/ROOT.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/General/ROOT.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -27,6 +27,7 @@
 use "ord_list.ML";
 use "balanced_tree.ML";
 use "graph.ML";
+use "binding.ML";
 use "name_space.ML";
 use "lazy.ML";
 use "path.ML";