equal
deleted
inserted
replaced
154 If bnd is true, then it replaces Bound variables only. *) |
154 If bnd is true, then it replaces Bound variables only. *) |
155 fun gen_hyp_subst_tac bnd = |
155 fun gen_hyp_subst_tac bnd = |
156 let fun tac i st = SUBGOAL (fn (Bi, _) => |
156 let fun tac i st = SUBGOAL (fn (Bi, _) => |
157 let |
157 let |
158 val (k, _) = eq_var bnd true Bi |
158 val (k, _) = eq_var bnd true Bi |
159 val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss |
159 val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss |
160 setmksimps (mk_eqs bnd) |
160 setmksimps (mk_eqs bnd) |
161 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, |
161 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, |
162 etac thin_rl i, rotate_tac (~k) i] |
162 etac thin_rl i, rotate_tac (~k) i] |
163 end handle THM _ => no_tac | EQ_VAR => no_tac) i st |
163 end handle THM _ => no_tac | EQ_VAR => no_tac) i st |
164 in REPEAT_DETERM1 o tac end; |
164 in REPEAT_DETERM1 o tac end; |