--- a/Nominal/Ex/Lambda.thy	Thu Jun 02 10:11:50 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 02 16:41:09 2011 +0900
@@ -531,16 +531,9 @@
   apply (rule, perm_simp, rule)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
   apply auto
-  apply (simp add: Abs1_eq_iff)
-  apply (auto)
+  apply (erule Abs1_eq_fdest)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
   apply (simp add: eqvt_def permute_fun_app_eq)
-  apply (drule supp_fun_app_eqvt)
-  apply (simp add: fresh_def )
-  apply blast
-  apply (simp add: eqvt_def permute_fun_app_eq)
-  apply (drule supp_fun_app_eqvt)
-  apply (simp add: fresh_def )
-  apply blast
   done
 
 termination
@@ -590,6 +583,7 @@
   Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 where
   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
+| "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
 unfolding eqvt_def Z_graph_def
 apply (rule, perm_simp, rule)
 oops
@@ -603,7 +597,7 @@
   "f [] = 0"
 | "f [e] = e"
 | "f (l @ m) = f l + f m"
-apply(simp_all)
+  apply(simp_all)
 oops