--- a/Admin/polyml/future/ROOT.ML Thu Aug 18 16:52:19 2011 +0900
+++ b/Admin/polyml/future/ROOT.ML Thu Aug 18 15:15:43 2011 +0200
@@ -78,6 +78,7 @@
use "General/table.ML";
use "General/graph.ML";
use "General/ord_list.ML";
+use "General/balanced_tree.ML";
structure Position =
struct