equal
deleted
inserted
replaced
129 fun gen_hyp_subst_tac bnd = |
129 fun gen_hyp_subst_tac bnd = |
130 let fun tac i st = SUBGOAL (fn (Bi, _) => |
130 let fun tac i st = SUBGOAL (fn (Bi, _) => |
131 let |
131 let |
132 val (k, _) = eq_var bnd true Bi |
132 val (k, _) = eq_var bnd true Bi |
133 val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss |
133 val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss |
134 setmksimps (K (mk_eqs bnd)) |
134 |> Simplifier.set_mksimps (K (mk_eqs bnd)) |
135 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, |
135 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, |
136 etac thin_rl i, rotate_tac (~k) i] |
136 etac thin_rl i, rotate_tac (~k) i] |
137 end handle THM _ => no_tac | EQ_VAR => no_tac) i st |
137 end handle THM _ => no_tac | EQ_VAR => no_tac) i st |
138 in REPEAT_DETERM1 o tac end; |
138 in REPEAT_DETERM1 o tac end; |
139 |
139 |