# HG changeset patch
# User berghofe
# Date 1108030743 -3600
# Node ID 81e5f6d3ab1d37d585691dc8dc02ce4bbbc92ff9
# Parent  3bc57d428ec1dd3b9ab088f7ccc7c5afbf246f61
Fixed bug in select_thm.

diff -r 3bc57d428ec1 -r 81e5f6d3ab1d src/Pure/pure_thy.ML
--- 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;