diff -r 8e1b14bf0190 -r e2741ec9ae36 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Tue Mar 20 21:37:31 2012 +0100
+++ b/src/Pure/General/seq.ML	Wed Mar 21 11:00:34 2012 +0100
@@ -167,7 +167,7 @@
 fun lift f xq y = map (fn x => f x y) xq;
 fun lifts f xq y = maps (fn x => f x y) xq;
 
-fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
+fun singleton f x = f [x] |> map (fn [y] => y | _ => raise List.Empty);
 
 (*print a sequence, up to "count" elements*)
 fun print print_elem count =