{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
solve the goal fully before proceeding

{HOL,ZF}/indrule/mutual_ind_tac: ensures that calls to "prem" cannot loop;
calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully

{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully

--- a/intr_elim.ML	Wed Oct 12 12:00:45 1994 +0100
+++ b/intr_elim.ML	Wed Oct 12 12:06:56 1994 +0100
@@ -83,8 +83,9 @@
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
    rtac disjIn 1,
-   (*Not ares_tac, since refl must be tried before any equality assumptions*)
-   REPEAT (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1)];
+   (*Not ares_tac, since refl must be tried before any equality assumptions;
+     backtracking may occur if the premises have extra variables!*)
+   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1)];
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls =