src/Pure/General/queue.ML

--- a/src/Pure/General/queue.ML	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/queue.ML	Wed Mar 21 11:00:34 2012 +0100
@@ -11,7 +11,7 @@
   val is_empty: 'a T -> bool
   val content: 'a T -> 'a list
   val enqueue: 'a -> 'a T -> 'a T
-  val dequeue: 'a T -> 'a * 'a T
+  val dequeue: 'a T -> 'a * 'a T  (*exception List.Empty*)
 end;
 
 structure Queue: QUEUE =
@@ -30,6 +30,6 @@
 
 fun dequeue (Queue (xs, y :: ys)) = (y, Queue (xs, ys))
   | dequeue (Queue (xs as _ :: _, [])) = let val y :: ys = rev xs in (y, Queue ([], ys)) end
-  | dequeue (Queue ([], [])) = raise Empty;
+  | dequeue (Queue ([], [])) = raise List.Empty;
 
 end;