diff -r 96c68fd7ed46 -r f745ff8bdb91 intr_elim.ML
--- 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 =