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