eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
--- 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 =
--- 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.*)