src/Pure/tctical.ML
changeset 2580 e3f680709487
parent 2244 dacee519738a
child 2627 4ee01bb55a44
     1.1 --- a/src/Pure/tctical.ML	Tue Feb 04 08:59:50 1997 +0100
     1.2 +++ b/src/Pure/tctical.ML	Tue Feb 04 10:33:58 1997 +0100
     1.3 @@ -304,10 +304,8 @@
     1.4  
     1.5  
     1.6  (*Make a tactic for subgoal i, if there is one.  *)
     1.7 -fun SUBGOAL goalfun i st = 
     1.8 -  case drop(i-1, prems_of st) of
     1.9 -      [] => Sequence.null
    1.10 -    | prem::_ => goalfun (prem,i) st;
    1.11 +fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
    1.12 +                             handle Subscript => Sequence.null;
    1.13  
    1.14  
    1.15  (*** SELECT_GOAL ***)
    1.16 @@ -346,9 +344,8 @@
    1.17  
    1.18  (*Does the work of SELECT_GOAL. *)
    1.19  fun select tac st0 i =
    1.20 -  let val cprem::_ = drop(i-1, cprems_of st0)
    1.21 -      val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
    1.22 -                                eq_trivial (adjust_maxidx cprem)
    1.23 +  let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
    1.24 +	  eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i-1)))
    1.25        fun next st = bicompose false (false, restore st, nprems_of st) i st0
    1.26    in  Sequence.flats (Sequence.maps next (tac eq_cprem))
    1.27    end;
    1.28 @@ -365,7 +362,7 @@
    1.29          handle _ => error"SELECT_GOAL -- impossible error???";
    1.30  
    1.31  fun SELECT_GOAL tac i st = 
    1.32 -  case (i, drop(i-1, prems_of st)) of
    1.33 +  case (i, List.drop(prems_of st, i-1)) of
    1.34        (_,[]) => Sequence.null
    1.35      | (1,[_]) => tac st         (*If i=1 and only one subgoal do nothing!*)
    1.36      | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i