# HG changeset patch
# User wenzelm
# Date 952172323 -3600
# Node ID 8f0f0ae02b10b2c7d6c0bcd1e27896f43f22cb01
# Parent  c169cd21fe42c35315e07e5d87f868af02bc66c4
added REPEAT_ALL_NEW;

diff -r c169cd21fe42 -r 8f0f0ae02b10 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Sat Mar 04 12:02:41 2000 +0100
+++ b/src/Pure/tctical.ML	Sat Mar 04 13:18:43 2000 +0100
@@ -57,6 +57,7 @@
   val THEN              : tactic * tactic -> tactic
   val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> 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
   val traced_tac        : (thm -> (thm * thm Seq.seq) option) -> tactic
   val tracify           : bool ref -> tactic -> tactic
@@ -358,6 +359,10 @@
 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'));
 
+(*repeatedly dig into any emerging subgoals*)
+fun REPEAT_ALL_NEW tac =
+  tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i));
+
 
 (*** SELECT_GOAL ***)