# HG changeset patch
# User wenzelm
# Date 1182287743 -7200
# Node ID 6f60a90e52e592999a746cf6c9ebbcc87566c561
# Parent  8c30dd4b3b220ac76fba80baf83b27054a2ade96
added General/balanced_tree.ML;

diff -r 8c30dd4b3b22 -r 6f60a90e52e5 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Tue Jun 19 23:15:38 2007 +0200
+++ b/src/Pure/General/ROOT.ML	Tue Jun 19 23:15:43 2007 +0200
@@ -8,6 +8,7 @@
 use "ord_list.ML";
 use "alist.ML";
 use "table.ML";
+use "balanced_tree.ML";
 use "output.ML";
 use "graph.ML";
 use "heap.ML";
diff -r 8c30dd4b3b22 -r 6f60a90e52e5 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jun 19 23:15:38 2007 +0200
+++ b/src/Pure/IsaMakefile	Tue Jun 19 23:15:43 2007 +0200
@@ -24,9 +24,9 @@
 Pure: $(OUT)/Pure$(ML_SUFFIX)
 
 $(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML		\
-  General/basics.ML General/buffer.ML General/file.ML General/graph.ML		\
-  General/heap.ML General/history.ML General/ml_syntax.ML General/name_space.ML	\
-  General/ord_list.ML General/output.ML General/path.ML				\
+  General/basics.ML General/balanced_tree.ML General/buffer.ML General/file.ML	\
+  General/graph.ML General/heap.ML General/history.ML General/ml_syntax.ML	\
+  General/name_space.ML General/ord_list.ML General/output.ML General/path.ML	\
   General/position.ML General/pretty.ML General/scan.ML		                \
   General/secure.ML General/seq.ML General/source.ML General/stack.ML		\
   General/susp.ML General/symbol.ML General/table.ML General/url.ML		\