--- 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 =