src/Pure/library.ML

--- a/src/Pure/library.ML	Wed Jun 08 15:39:55 2011 +0200
+++ b/src/Pure/library.ML	Wed Jun 08 15:56:57 2011 +0200
@@ -429,7 +429,7 @@
   raise Subscript if list too short*)
 fun nth xs i = List.nth (xs, i);
 
-fun nth_list xss i = nth xss i handle Subscript => [];
+fun nth_list xss i = nth xss i handle General.Subscript => [];
 
 fun nth_map 0 f (x :: xs) = f x :: xs
   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs