ALLGOALS_RANGE superceded by Seq.INTERVAL;
authorwenzelm
Mon Mar 20 18:46:53 2000 +0100 (2000-03-20)
changeset 85357428194b39f7
parent 8534 fdbabfbc3829
child 8536 de307f5bc89a
ALLGOALS_RANGE superceded by Seq.INTERVAL;
src/Pure/General/seq.ML
src/Pure/tctical.ML
     1.1 --- a/src/Pure/General/seq.ML	Mon Mar 20 18:45:28 2000 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Mon Mar 20 18:46:53 2000 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    val TRY: ('a -> 'a seq) -> 'a -> 'a seq
     1.5    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
     1.6    val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
     1.7 +  val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
     1.8  end;
     1.9  
    1.10  structure Seq: SEQ =
    1.11 @@ -217,4 +218,9 @@
    1.12  fun REPEAT1 f = THEN (f, REPEAT f);
    1.13  
    1.14  
    1.15 +fun INTERVAL f i j x =
    1.16 +  if i > j then single x
    1.17 +  else op THEN (f j, INTERVAL f i (j - 1)) x;
    1.18 +
    1.19 +
    1.20  end;
     2.1 --- a/src/Pure/tctical.ML	Mon Mar 20 18:45:28 2000 +0100
     2.2 +++ b/src/Pure/tctical.ML	Mon Mar 20 18:46:53 2000 +0100
     2.3 @@ -56,7 +56,6 @@
     2.4    val suppress_tracing  : bool ref
     2.5    val THEN              : tactic * tactic -> tactic
     2.6    val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
     2.7 -  val ALLGOALS_RANGE    : (int -> tactic) -> int -> int -> tactic
     2.8    val THEN_ALL_NEW	: (int -> tactic) * (int -> tactic) -> int -> tactic
     2.9    val REPEAT_ALL_NEW	: (int -> tactic) -> int -> tactic
    2.10    val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
    2.11 @@ -353,12 +352,8 @@
    2.12      in  Seq.filter diff (tac i st)  end
    2.13      handle Subscript => Seq.empty  (*no subgoal i*);
    2.14  
    2.15 -fun ALLGOALS_RANGE tac (i:int) j st =
    2.16 -  if i > j then all_tac st
    2.17 -  else (tac j THEN ALLGOALS_RANGE tac i (j - 1)) st;
    2.18 -
    2.19  fun (tac1 THEN_ALL_NEW tac2) i st =
    2.20 -  st |> (tac1 i THEN (fn st' => ALLGOALS_RANGE tac2 i (i + nprems_of st' - nprems_of st) st'));
    2.21 +  st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'));
    2.22  
    2.23  (*repeatedly dig into any emerging subgoals*)
    2.24  fun REPEAT_ALL_NEW tac =