Prevent permutation of assumptions in hyp_subst_tac
authorpaulson
Fri Mar 07 10:22:54 1997 +0100 (1997-03-07 ago)
changeset 2750fe3799355b5e
parent 2749 2f477a0e690d
child 2751 673c4eefd2e1
Prevent permutation of assumptions in hyp_subst_tac
src/Provers/hypsubst.ML
     1.1 --- a/src/Provers/hypsubst.ML	Fri Mar 07 10:21:11 1997 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Fri Mar 07 10:22:54 1997 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4  		etac revcut_rl i,
     1.5  		REPEAT_DETERM_N (n-k) (etac rev_mp i),
     1.6  		etac (if symopt then ssubst else subst) i,
     1.7 -		REPEAT_DETERM_N n (rtac imp_intr i)]
     1.8 +		REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]
     1.9        end
    1.10        handle THM _ => no_tac | EQ_VAR => no_tac));
    1.11