intro_tacsf: replaced ORELSE by APPEND in order to stop
errors that arise when unconstrained equalities appear in the premises. Could
cause runtimes to increase...

--- a/src/HOL/intr_elim.ML	Mon Dec 16 10:35:51 1996 +0100
+++ b/src/HOL/intr_elim.ML	Mon Dec 16 10:40:14 1996 +0100
@@ -88,7 +88,7 @@
    rtac disjIn 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),
+   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
    (*Now solve the equations like Inl 0 = Inl ?b2*)
    rewrite_goals_tac Inductive.con_defs,
    REPEAT (rtac refl 1)];

--- a/src/ZF/intr_elim.ML	Mon Dec 16 10:35:51 1996 +0100
+++ b/src/ZF/intr_elim.ML	Mon Dec 16 10:40:14 1996 +0100
@@ -104,7 +104,7 @@
    rtac disjIn 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),
+   DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),
    (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
    rewrite_goals_tac Inductive.con_defs,
    REPEAT (rtac refl 2),