--- a/Nominal/Ex/Lambda.thy	Thu Jun 02 12:09:31 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 02 12:14:03 2011 +0100
@@ -561,16 +561,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
@@ -620,6 +613,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
@@ -633,7 +627,7 @@
   "f [] = 0"
 | "f [e] = e"
 | "f (l @ m) = f l + f m"
-apply(simp_all)
+  apply(simp_all)
 oops