--- a/Nominal/Rsp.thy Wed May 12 13:43:48 2010 +0100
+++ b/Nominal/Rsp.thy Wed May 12 16:08:32 2010 +0200
@@ -60,7 +60,7 @@
ML {*
fun fvbv_rsp_tac induct fvbv_simps ctxt =
- rel_indtac induct THEN_ALL_NEW
+ rtac induct THEN_ALL_NEW
(TRY o rtac @{thm TrueI}) THEN_ALL_NEW
asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW
@@ -96,7 +96,7 @@
ML {*
fun alpha_eqvt_tac induct simps ctxt =
- rel_indtac induct THEN_ALL_NEW
+ rtac induct THEN_ALL_NEW
simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW