diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/General/balanced_tree.ML
--- a/src/Pure/General/balanced_tree.ML	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/balanced_tree.ML	Wed Mar 21 11:00:34 2012 +0100
@@ -15,7 +15,7 @@
 structure Balanced_Tree: BALANCED_TREE =
 struct
 
-fun make _ [] = raise Empty
+fun make _ [] = raise List.Empty
   | make _ [x] = x
   | make f xs =
       let
@@ -24,7 +24,7 @@
       in f (make f ps, make f qs) end;
 
 fun dest f n x =
-  if n <= 0 then raise Empty
+  if n <= 0 then raise List.Empty
   else if n = 1 then [x]
   else
     let