--- a/Nominal/Abs.thy	Mon Mar 22 18:38:59 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 23 07:39:10 2010 +0100
@@ -118,22 +118,6 @@
   by (rule_tac x="(a \<rightleftharpoons> b)" in exI)
      (auto simp add: supp_perm swap_atom)
 
-lemma alpha_gen_swap_fun:
-  assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"
-  assumes a1: "a \<notin> (f x) - bs"
-  and     a2: "b \<notin> (f x) - bs"
-  shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
-  apply(simp add: alpha_gen)
-  apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric])
-  apply(simp add: swap_set_not_in[OF a1 a2])
-  apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
-  using a1 a2
-  apply(simp add: fresh_star_def fresh_def)
-  apply(blast)
-  apply(simp add: supp_swap)
-  done
-
 fun
   supp_abs_fun
 where