diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/stack.ML	Wed Mar 21 11:00:34 2012 +0100
@@ -13,7 +13,7 @@
   val map_top: ('a -> 'a) -> 'a T -> 'a T
   val map_all: ('a -> 'a) -> 'a T -> 'a T
   val push: 'a T -> 'a T
-  val pop: 'a T -> 'a T      (*exception Empty*)
+  val pop: 'a T -> 'a T      (*exception List.Empty*)
 end;
 
 structure Stack: STACK =
@@ -34,6 +34,6 @@
 fun push (x, xs) = (x, x :: xs);
 
 fun pop (_, x :: xs) = (x, xs)
-  | pop (_, []) = raise Empty;
+  | pop (_, []) = raise List.Empty;
 
 end;