| changeset 15518 | 81e5f6d3ab1d |
| parent 15517 | 3bc57d428ec1 |
| child 15531 | 08c8dad8e399 |
--- a/src/Pure/pure_thy.ML Thu Feb 10 10:43:57 2005 +0100 +++ b/src/Pure/pure_thy.ML Thu Feb 10 11:19:03 2005 +0100 @@ -143,7 +143,7 @@ fun select_thm (s, None) xs = xs | select_thm (s, Some is) xs = map - (fn i => if i < 1 then raise LIST "" else nth_elem (i-1, 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;