src/Pure/tctical.ML
changeset 709 0d0df9b5afe3
parent 703 3a5cd2883581
child 729 cc4c4eafe628
equal deleted inserted replaced
708:8422e50adce0 709:0d0df9b5afe3
   442       ([state'],_) => state'
   442       ([state'],_) => state'
   443     | _            => error"SELECT_GOAL -- impossible error???";
   443     | _            => error"SELECT_GOAL -- impossible error???";
   444 
   444 
   445 (*Does the work of SELECT_GOAL. *)
   445 (*Does the work of SELECT_GOAL. *)
   446 fun select (Tactic tf) state i =
   446 fun select (Tactic tf) state i =
   447   let val prem::_ = drop(i-1, prems_of state)
   447   let val cprem::_ = drop(i-1, cprems_of state)
   448       val st0 = trivial (cterm_of (#sign(rep_thm state)) prem);
       
   449       fun next st = bicompose false (false, st, nprems_of st) i state
   448       fun next st = bicompose false (false, st, nprems_of st) i state
   450   in  Sequence.flats (Sequence.maps next (tf st0))
   449   in  Sequence.flats (Sequence.maps next (tf (trivial cprem)))
   451   end;
   450   end;
   452 
   451 
   453 fun SELECT_GOAL tac i = Tactic (fn state =>
   452 fun SELECT_GOAL tac i = Tactic (fn state =>
   454   case (i, drop(i-1, prems_of state)) of
   453   case (i, drop(i-1, prems_of state)) of
   455       (_,[]) => Sequence.null
   454       (_,[]) => Sequence.null