--- a/Nominal/Rsp.thy	Thu Mar 11 10:39:29 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 11:15:14 2010 +0100
@@ -120,7 +120,17 @@
 *)
 
 ML {*
-fun build_eqvts bind funs simps induct ctxt =
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+
+ML {*
+fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
+*}
+
+ML {*
+fun build_eqvts bind funs tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
@@ -131,10 +141,7 @@
   fun eqvtc (fnctn, arg) =
     HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
-  fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
-  val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
+  val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames)
   val thms = HOLogic.conj_elims thm
 in
   Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
@@ -147,9 +154,6 @@
 by auto
 
 ML {*
-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)
@@ -196,8 +200,8 @@
 *}
 
 ML {*
-fun build_bv_eqvt simps inducts (t, n) =
-  build_eqvts Binding.empty [t] simps (nth inducts n)
+fun build_bv_eqvt simps inducts (t, n) ctxt =
+  build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt
 *}
 
 end