changeset 2750 | fe3799355b5e |
parent 2722 | 3e07c20b967c |
child 3537 | 79ac9b475621 |
--- a/src/Provers/hypsubst.ML Fri Mar 07 10:21:11 1997 +0100 +++ b/src/Provers/hypsubst.ML Fri Mar 07 10:22:54 1997 +0100 @@ -168,7 +168,7 @@ etac revcut_rl i, REPEAT_DETERM_N (n-k) (etac rev_mp i), etac (if symopt then ssubst else subst) i, - REPEAT_DETERM_N n (rtac imp_intr i)] + REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)] end handle THM _ => no_tac | EQ_VAR => no_tac));