--- a/Nominal/Rsp.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -125,37 +125,14 @@
 *)
 
 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 perm_arg arg =
 let
   val ty = fastype_of arg
 in
   Const (@{const_name permute}, @{typ perm} --> ty --> ty)
 end
-*}
 
-
-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 types);
-  val args = map Free (indnames ~~ types);
-  val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  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
-end
+val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
 *}
 
 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"