--- a/intr_elim.ML Wed Sep 07 13:17:34 1994 +0200
+++ b/intr_elim.ML Thu Sep 08 11:01:45 1994 +0200
@@ -83,7 +83,8 @@
REPEAT (resolve_tac [Part_eqI,CollectI] 1),
(*Now 1-2 subgoals: the disjunction, perhaps equality.*)
rtac disjIn 1,
- REPEAT (ares_tac [refl,exI,conjI] 1)];
+ (*Not ares_tac, since refl must be tried before any equality assumptions*)
+ REPEAT (resolve_tac [refl,exI,conjI] 1 ORELSE assume_tac 1)];
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
val mk_disj_rls =