diff -r 409ecb7284dd -r c5b7be27f105 Nominal/Rsp.thy
--- 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