--- a/Nominal/Nominal2_Base.thy	Tue Jun 12 13:56:16 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 12 14:22:58 2012 +0100
@@ -1225,12 +1225,16 @@
 
 subsubsection {* Equivariance for @{typ "('a, 'b) finfun"} *}
 
-lemma permute_finfun_update[eqvt]:
+lemma finfun_update_eqvt [eqvt]:
   shows "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)"
 by (transfer) (simp)
 
-lemma permute_finfun_const[eqvt]:
-  shows "(p \<bullet> (finfun_const b)) = (finfun_const (p \<bullet> b))"
+lemma finfun_const_eqvt [eqvt]:
+  shows "(p \<bullet> (finfun_const b)) = finfun_const (p \<bullet> b)"
+by (transfer) (simp)
+
+lemma finfun_apply_eqvt [eqvt]:
+  shows "(p \<bullet> (finfun_apply f b)) = finfun_apply (p \<bullet> f) (p \<bullet> b)"
 by (transfer) (simp)
 
 
@@ -2239,7 +2243,7 @@
 lemma fresh_finfun_update:
   shows "\<lbrakk>a \<sharp> f; a \<sharp> x; a \<sharp> y\<rbrakk> \<Longrightarrow> a \<sharp> finfun_update f x y"
   unfolding fresh_conv_MOST
-  unfolding permute_finfun_update
+  unfolding finfun_update_eqvt
   by (elim MOST_rev_mp) (simp)
 
 lemma supp_finfun_const: