tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;

--- a/src/Pure/tctical.ML	Tue Jun 21 09:31:57 2005 +0200
+++ b/src/Pure/tctical.ML	Tue Jun 21 09:35:30 2005 +0200
@@ -342,8 +342,10 @@
 
 
 (*Make a tactic for subgoal i, if there is one.  *)
-fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
-                             handle Subscript => Seq.empty;
+fun SUBGOAL goalfun i st =
+  (case try Logic.nth_prem (i, Thm.prop_of st) of
+    SOME goal => goalfun (goal, i) st
+  | NONE => Seq.empty);
 
 (*Returns all states that have changed in subgoal i, counted from the LAST
   subgoal.  For stac, for example.*)