--- a/Nominal-General/Nominal2_Base.thy	Fri Apr 23 11:12:38 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Sat Apr 24 09:49:23 2010 +0200
@@ -1081,12 +1081,18 @@
   unfolding fresh_def
   by auto
 
+lemma supp_fun_eqvt:
+  assumes a: "\<forall>p. p \<bullet> f = f"
+  shows "supp f = {}"
+  unfolding supp_def 
+  using a by simp
+
+
 lemma fresh_fun_eqvt_app:
   assumes a: "\<forall>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
-  from a have "supp f = {}"
-    unfolding supp_def by simp
+  from a have "supp f = {}" by (simp add: supp_fun_eqvt)
   then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
     unfolding fresh_def
     using supp_fun_app