# HG changeset patch
# User wenzelm
# Date 1329335790 -3600
# Node ID bf96ed9e55c1d054bedabedd04e6200754406f1a
# Parent  c505ea79e2db27efae1832d5032c348c1b068724
eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);

diff -r c505ea79e2db -r bf96ed9e55c1 src/Pure/search.ML
--- a/src/Pure/search.ML	Wed Feb 15 20:47:32 2012 +0100
+++ b/src/Pure/search.ML	Wed Feb 15 20:56:30 2012 +0100
@@ -13,7 +13,6 @@
   val has_fewer_prems: int -> thm -> bool
   val IF_UNSOLVED: tactic -> tactic
   val SOLVE: tactic -> tactic
-  val DETERM_UNTIL_SOLVED: tactic -> tactic
   val THEN_MAYBE: tactic * tactic -> tactic
   val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val DEPTH_SOLVE: tactic -> tactic
@@ -65,9 +64,6 @@
 (*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 =
diff -r c505ea79e2db -r bf96ed9e55c1 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Wed Feb 15 20:47:32 2012 +0100
+++ b/src/Pure/tactical.ML	Wed Feb 15 20:56:30 2012 +0100
@@ -36,7 +36,6 @@
   val suppress_tracing: bool Unsynchronized.ref
   val tracify: bool Unsynchronized.ref -> tactic -> tactic
   val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
-  val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic
   val REPEAT_DETERM_N: int -> tactic -> tactic
   val REPEAT_DETERM: tactic -> tactic
   val REPEAT: tactic -> tactic
@@ -235,16 +234,6 @@
                          handle TRACE_EXIT st' => SOME(st', Seq.empty)));
 
 
-(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive.
-  Forces repitition until predicate on state is fulfilled.*)
-fun DETERM_UNTIL p tac =
-let val tac = tracify trace_REPEAT tac
-    fun drep st = if p st then SOME (st, Seq.empty)
-                          else (case Seq.pull(tac st) of
-                                  NONE        => NONE
-                                | SOME(st',_) => drep st')
-in  traced_tac drep  end;
-
 (*Deterministic REPEAT: only retains the first outcome;
   uses less space than REPEAT; tail recursive.
   If non-negative, n bounds the number of repetitions.*)