# HG changeset patch
# User wenzelm
# Date 1119339330 -7200
# Node ID 606d919ad3c3d8c5ad5c436b1aeee55b6560544d
# Parent  20f4c6a950f7d93320dd130590be2ea42e2cafed
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;

diff -r 20f4c6a950f7 -r 606d919ad3c3 src/Pure/tctical.ML
--- 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.*)