diff -r c6e521a2a0b1 -r 80441e27dfd6 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Wed Mar 03 15:28:25 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 03 17:47:29 2010 +0100
@@ -146,7 +146,9 @@
 by auto
 
 ML {*
-  fun indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+ML {*
   fun all_eqvts ctxt =
     Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
   val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
@@ -161,7 +163,7 @@
 
 ML {*
 fun alpha_eqvt_tac induct simps ctxt =
-  indtac induct THEN_ALL_NEW
+  ind_tac induct THEN_ALL_NEW
   simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW