--- a/Nominal/Equivp.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Equivp.thy	Wed May 26 15:34:54 2010 +0200
@@ -340,28 +340,6 @@
 
 
 
-ML {*
-fun build_eqvt_gl pi frees fnctn ctxt =
-let
-  val typ = domain_type (fastype_of fnctn);
-  val arg = the (AList.lookup (op=) frees typ);
-in
-  ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)
-end
-*}
 
-ML {*
-fun prove_eqvt tys ind simps funs ctxt =
-let
-  val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
-  val pi = Free (pi, @{typ perm});
-  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
-  val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
-  val ths = Variable.export ctxt' ctxt ths_loc
-  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
-in
-  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
-end
-*}
 
 end