diff -r f8d660de0cf7 -r 1ae3c9b2d557 Nominal/Ex/Lambda_F_T.thy
--- a/Nominal/Ex/Lambda_F_T.thy	Thu Jun 09 15:34:51 2011 +0900
+++ b/Nominal/Ex/Lambda_F_T.thy	Fri Jun 10 15:30:09 2011 +0900
@@ -9,27 +9,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
-lemma Abs1_eq_fdest:
-  fixes x y :: "'a :: at_base"
-    and S T :: "'b :: fs"
-  assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
-  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
-  and "sort_of (atom x) = sort_of (atom y)"
-  shows "f x T = f y S"
-using assms apply -
-apply (subst (asm) Abs1_eq_iff')
-apply simp_all
-apply (elim conjE disjE)
-apply simp
-apply(rule trans)
-apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(simp add: supp_swap fresh_star_def)
-apply(simp add: swap_commute)
-done
-
 lemma fresh_fun_eqvt_app3:
   assumes a: "eqvt f"
   and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
@@ -89,7 +68,7 @@
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)
-  apply(erule Abs1_eq_fdest)
+  apply(erule Abs_lst1_fcb)
   apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la")
   apply (simp add: fresh_star_def)
   apply (rule fcb3)