tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
authorwenzelm
Tue Jun 21 09:35:30 2005 +0200 (2005-06-21)
changeset 16510606d919ad3c3
parent 16509 20f4c6a950f7
child 16511 dad516b121cd
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
src/Pure/tctical.ML
     1.1 --- a/src/Pure/tctical.ML	Tue Jun 21 09:31:57 2005 +0200
     1.2 +++ b/src/Pure/tctical.ML	Tue Jun 21 09:35:30 2005 +0200
     1.3 @@ -342,8 +342,10 @@
     1.4  
     1.5  
     1.6  (*Make a tactic for subgoal i, if there is one.  *)
     1.7 -fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
     1.8 -                             handle Subscript => Seq.empty;
     1.9 +fun SUBGOAL goalfun i st =
    1.10 +  (case try Logic.nth_prem (i, Thm.prop_of st) of
    1.11 +    SOME goal => goalfun (goal, i) st
    1.12 +  | NONE => Seq.empty);
    1.13  
    1.14  (*Returns all states that have changed in subgoal i, counted from the LAST
    1.15    subgoal.  For stac, for example.*)