--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 21 21:31:07 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 21 21:52:30 2010 +0200
@@ -1079,26 +1079,6 @@
   unfolding fresh_def
   by auto
 
-(* alternative proof *)
-lemma 
-  shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
-proof (rule subsetCI)
-  fix a::"atom"
-  assume a: "a \<in> supp (f x)"
-  assume b: "a \<notin> supp f \<union> supp x"
-  then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" 
-    unfolding supp_def by auto
-  then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp
-  moreover 
-  have "{b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x} \<subseteq> ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})"
-    by auto
-  ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}"
-    using finite_subset by auto
-  then have "a \<notin> supp (f x)" unfolding supp_def
-    by (simp add: permute_fun_app_eq)
-  with a show "False" by simp
-qed
-    
 lemma fresh_fun_eqvt_app:
   assumes a: "\<forall>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"