# HG changeset patch
# User wenzelm
# Date 1141503008 -3600
# Node ID 3e30297e13004e971b90e02fe5a0967f1e968333
# Parent  3421668ae316d8dfcf2cd851f94c9384b88107d7
added extract, retrofit;

diff -r 3421668ae316 -r 3e30297e1300 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Mar 04 21:10:07 2006 +0100
+++ b/src/Pure/goal.ML	Sat Mar 04 21:10:08 2006 +0100
@@ -26,6 +26,8 @@
     (thm list -> tactic) -> thm list
   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
+  val extract: int -> int -> thm -> thm Seq.seq
+  val retrofit: int -> int -> thm -> thm -> thm Seq.seq
 end;
 
 structure Goal: GOAL =
@@ -168,30 +170,23 @@
   | NONE => error "Tactic failed.");
 
 
-(* 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 thm with the original state.*)
-
-local
+(** local goal states **)
 
-fun SELECT tac i st =
-  init (Thm.adjust_maxidx (Thm.cprem_of st i))
-  |> tac
-  |> Seq.maps (fn st' =>
-    Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i st);
+fun extract i n st =
+  (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
+   else if n = 1 then Seq.single (Thm.cprem_of st i)
+   else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
+  |> Seq.map (Thm.adjust_maxidx #> init);
 
-in
+fun retrofit i n st' =
+  (if n = 1 then I
+   else Drule.rotate_prems (i - 1) #> Drule.conj_uncurry n #> Drule.rotate_prems (1 - i))
+  #> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
 
 fun SELECT_GOAL tac i st =
-  let val n = Thm.nprems_of st in
-    if 1 <= i andalso i <= n then
-      if n = 1 then tac st else SELECT tac i st
-    else Seq.empty
-  end;
-
-end;
+  if Thm.nprems_of st = 1 then tac st
+  else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
 
 end;