diff -r 5ef0b624aadb -r 941afb897532 src/Pure/search.ML
--- a/src/Pure/search.ML	Fri Jan 28 11:22:02 2000 +0100
+++ b/src/Pure/search.ML	Fri Jan 28 11:23:41 2000 +0100
@@ -24,6 +24,7 @@
   val has_fewer_prems	: int -> thm -> bool   
   val IF_UNSOLVED	: tactic -> tactic
   val SOLVE		: tactic -> tactic
+  val DETERM_UNTIL_SOLVED: tactic -> tactic
   val trace_BEST_FIRST	: bool ref
   val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
   val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
@@ -69,6 +70,9 @@
 (*Force a tactic to solve its goal completely, otherwise fail *)
 fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
 
+(*Force repeated application of tactic until goal is solved completely *)
+val DETERM_UNTIL_SOLVED = DETERM_UNTIL (has_fewer_prems 1);
+
 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
 fun (tac1 THEN_MAYBE tac2) st =