diff -r c0e62be6ef04 -r 7d8781fc2c8e intr_elim.ML
--- 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 =