src/Provers/hypsubst.ML

--- 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));