# HG changeset patch
# User wenzelm
# Date 1129911289 -7200
# Node ID 7262f4a4519020c918b5462bae7f027bddf59e60
# Parent  d50f08d9aabbd602e3c1c05f71de665f30ab78bb
moved SELECT_GOAL to goal.ML;

diff -r d50f08d9aabb -r 7262f4a45190 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Oct 21 18:14:48 2005 +0200
+++ b/src/Pure/tctical.ML	Fri Oct 21 18:14:49 2005 +0200
@@ -52,7 +52,6 @@
   val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
   val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
   val DETERM_UNTIL      : (thm -> bool) -> tactic -> tactic
-  val SELECT_GOAL       : tactic -> int -> tactic
   val SINGLE            : tactic -> thm -> thm option
   val SOMEGOAL          : (int -> tactic) -> tactic
   val strip_context     : term -> (string * typ) list * term list * term
@@ -369,30 +368,6 @@
   tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
 
 
-(*** SELECT_GOAL ***)
-
-(*Tactical for restricting the effect of a tactic to subgoal i.
-  Works by making a new state from subgoal i, applying tac to it, and
-  composing the resulting metathm with the original state.*)
-
-(*Does the work of SELECT_GOAL. *)
-fun select tac st i =
-  let
-    val thm = Drule.mk_triv_goal (adjust_maxidx (List.nth (cprems_of st, i-1)));
-    fun restore th = Seq.hd (bicompose false (false, th, nprems_of th) 1
-      (Thm.incr_indexes (#maxidx (rep_thm th) + 1) Drule.rev_triv_goal));
-    fun next st' = bicompose false (false, restore st', nprems_of st') i st;
-  in Seq.maps next (tac thm) end;
-
-fun SELECT_GOAL tac i st =
-  let val np = nprems_of st
-  in  if 1<=i andalso i<=np then
-          (*If only one subgoal, then just apply tactic*)
-          if np=1 then tac st else select tac st i
-      else Seq.empty
-  end;
-
-
 (*Strips assumptions in goal yielding  ( [x1,...,xm], [H1,...,Hn], B )
     H1,...,Hn are the hypotheses;  x1...xm are variants of the parameters.
   Main difference from strip_assums concerns parameters: