# HG changeset patch
# User wenzelm
# Date 953574413 -3600
# Node ID 7428194b39f7b8b081161a19d84edaff6ff9a1af
# Parent  fdbabfbc382955eb8f88357b830ec0ba6368f4d1
ALLGOALS_RANGE superceded by Seq.INTERVAL;

diff -r fdbabfbc3829 -r 7428194b39f7 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Mon Mar 20 18:45:28 2000 +0100
+++ b/src/Pure/General/seq.ML	Mon Mar 20 18:46:53 2000 +0100
@@ -39,6 +39,7 @@
   val TRY: ('a -> 'a seq) -> 'a -> 'a seq
   val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
   val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
+  val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
 end;
 
 structure Seq: SEQ =
@@ -217,4 +218,9 @@
 fun REPEAT1 f = THEN (f, REPEAT f);
 
 
+fun INTERVAL f i j x =
+  if i > j then single x
+  else op THEN (f j, INTERVAL f i (j - 1)) x;
+
+
 end;
diff -r fdbabfbc3829 -r 7428194b39f7 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Mar 20 18:45:28 2000 +0100
+++ b/src/Pure/tctical.ML	Mon Mar 20 18:46:53 2000 +0100
@@ -56,7 +56,6 @@
   val suppress_tracing  : bool ref
   val THEN              : tactic * tactic -> tactic
   val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val ALLGOALS_RANGE    : (int -> tactic) -> int -> int -> tactic
   val THEN_ALL_NEW	: (int -> tactic) * (int -> tactic) -> int -> tactic
   val REPEAT_ALL_NEW	: (int -> tactic) -> int -> tactic
   val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
@@ -353,12 +352,8 @@
     in  Seq.filter diff (tac i st)  end
     handle Subscript => Seq.empty  (*no subgoal i*);
 
-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'));
+  st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'));
 
 (*repeatedly dig into any emerging subgoals*)
 fun REPEAT_ALL_NEW tac =