added THEN_ALL_NEW;

--- a/src/Pure/tctical.ML	Thu Feb 05 10:48:43 1998 +0100
+++ b/src/Pure/tctical.ML	Thu Feb 05 11:19:51 1998 +0100
@@ -6,7 +6,7 @@
 Tacticals
 *)
 
-infix 1 THEN THEN';
+infix 1 THEN THEN' THEN_ALL_NEW;
 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
 infix 0 THEN_ELSE;
 
@@ -54,6 +54,7 @@
   val suppress_tracing  : bool ref
   val THEN              : tactic * tactic -> tactic
   val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+  val THEN_ALL_NEW	: (int -> tactic) * (int -> tactic) -> int -> tactic
   val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
   val traced_tac        : (thm -> (thm * thm Seq.seq) option) -> tactic
   val tracify           : bool ref -> tactic -> thm -> thm Seq.seq
@@ -322,6 +323,13 @@
 fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
                              handle Subscript => Seq.empty;
 
+fun ALLGOALS_RANGE tac (i:int) j st =
+  if i > j then all_tac st
+  else (tac j THEN ALLGOALS_RANGE tac i (j - 1)) st;
+
+fun (tac1 THEN_ALL_NEW tac2) i st =
+  st |> (tac1 i THEN (fn st' => ALLGOALS_RANGE tac2 i (i + nprems_of st' - nprems_of st) st'));
+
 
 (*** SELECT_GOAL ***)