src/Pure/library.ML
changeset 43278 1fbdcebb364b
parent 42403 38b29c9fc742
child 43559 c1966f322105
     1.1 --- a/src/Pure/library.ML	Wed Jun 08 15:39:55 2011 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Jun 08 15:56:57 2011 +0200
     1.3 @@ -429,7 +429,7 @@
     1.4    raise Subscript if list too short*)
     1.5  fun nth xs i = List.nth (xs, i);
     1.6  
     1.7 -fun nth_list xss i = nth xss i handle Subscript => [];
     1.8 +fun nth_list xss i = nth xss i handle General.Subscript => [];
     1.9  
    1.10  fun nth_map 0 f (x :: xs) = f x :: xs
    1.11    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs