--- a/Nominal/Rsp.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -87,13 +87,18 @@
 *}
 
 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)
+*}
+
+ML {*
 fun constr_rsp_tac inj rsp equivps =
 let
   val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
 in
   REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN'
-  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
    rtac @{thm exI[of _ "0 :: perm"]} THEN'
    asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
@@ -120,20 +125,28 @@
 *)
 
 ML {*
-fun build_eqvts bind funs perms 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;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
+  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun eqvtc (fnctn, (arg, perm)) =
-    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
-  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
+  fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
+  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)))
+  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
@@ -145,14 +158,6 @@
 apply (rule_tac x="pi \<bullet> pia" in exI)
 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)
-*}
 
 ML {*
 fun mk_minimal_ss ctxt =
@@ -195,8 +200,8 @@
 *}
 
 ML {*
-fun build_bv_eqvt perms simps inducts (t, n) =
-  build_eqvts Binding.empty [t] [nth perms n] 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