--- a/Nominal/Fv.thy	Sat Mar 27 12:20:17 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 12:26:59 2010 +0100
@@ -944,7 +944,7 @@
   val typ = domain_type (fastype_of fnctn);
   val arg = the (AList.lookup (op=) frees typ);
 in
-  ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
+  ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
 end
 *}
 
@@ -953,7 +953,7 @@
 let
   val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
   val pi = Free (pi, @{typ perm});
-  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt'))
+  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)