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.*)