# HG changeset patch
# User paulson
# Date 857726574 -3600
# Node ID fe3799355b5e56b02eb7a124f8c8dc0082011cd1
# Parent  2f477a0e690d35ed9e35c4daa074422feb55a292
Prevent permutation of assumptions in hyp_subst_tac

diff -r 2f477a0e690d -r fe3799355b5e 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));