# HG changeset patch
# User lcp
# Date 781960818 -3600
# Node ID 8a5f6961250f34a98257a50caddeb76dc0e746b9
# Parent  9e4d4f3eb812c090e6772cee35642f5cd288491b
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully

diff -r 9e4d4f3eb812 -r 8a5f6961250f src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Wed Oct 12 12:09:54 1994 +0100
+++ b/src/ZF/intr_elim.ML	Wed Oct 12 12:20:18 1994 +0100
@@ -92,8 +92,9 @@
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
    rtac disjIn 2,
-   (*Not ares_tac, since refl must be tried before any equality assumptions*)
-   REPEAT (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2),
+   (*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] 2 ORELSE assume_tac 2),
    (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
    rewrite_goals_tac con_defs,
    REPEAT (rtac refl 2),