src/Pure/pure_thy.ML
changeset 15517 3bc57d428ec1
parent 15456 956d6acacf89
child 15518 81e5f6d3ab1d
--- 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;