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