src/Provers/hypsubst.ML
changeset 2750 fe3799355b5e
parent 2722 3e07c20b967c
child 3537 79ac9b475621
equal deleted inserted replaced
2749:2f477a0e690d 2750:fe3799355b5e
   166       in 
   166       in 
   167 	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
   167 	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
   168 		etac revcut_rl i,
   168 		etac revcut_rl i,
   169 		REPEAT_DETERM_N (n-k) (etac rev_mp i),
   169 		REPEAT_DETERM_N (n-k) (etac rev_mp i),
   170 		etac (if symopt then ssubst else subst) i,
   170 		etac (if symopt then ssubst else subst) i,
   171 		REPEAT_DETERM_N n (rtac imp_intr i)]
   171 		REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]
   172       end
   172       end
   173       handle THM _ => no_tac | EQ_VAR => no_tac));
   173       handle THM _ => no_tac | EQ_VAR => no_tac));
   174 
   174 
   175 (*Substitutes for Free or Bound variables*)
   175 (*Substitutes for Free or Bound variables*)
   176 val hyp_subst_tac = 
   176 val hyp_subst_tac =