diff -r a4bbed7487ea -r 3bc57d428ec1 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Feb 10 08:25:22 2005 +0100 +++ b/src/Pure/pure_thy.ML Thu Feb 10 10:43:57 2005 +0100 @@ -143,7 +143,7 @@ fun select_thm (s, None) xs = xs | select_thm (s, Some is) xs = map - (fn i => nth_elem (i, xs) handle LIST _ => + (fn i => if i < 1 then raise LIST "" else nth_elem (i-1, xs) handle LIST _ => error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote s)) is;