--- a/Nominal/Ex/Foo2.thy	Mon Nov 29 08:01:09 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Fri Dec 03 13:51:07 2010 +0000
@@ -64,7 +64,6 @@
   tests by cu
 *}
 
-
 lemma yy:
   assumes a: "p \<bullet> bs \<inter> bs = {}" 
   and     b: "finite bs"
@@ -100,6 +99,8 @@
 apply(simp add: mem_permute_iff)
 done
 
+
+
 lemma Abs_rename_set:
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
@@ -217,7 +218,7 @@
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
   and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
-  and     "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
+  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
   and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
   shows "P"
@@ -230,7 +231,6 @@
 apply(assumption)
 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
 apply(erule exE)
-apply(rule assms(3))
 apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name]" in meta_spec)
@@ -239,12 +239,14 @@
 apply(drule meta_mp)
 apply(simp)
 apply(erule exE)
-apply(rule exI)+
+apply(rule assms(3))
 apply(perm_simp)
 apply(erule conjE)+
-apply(rule conjI)
 apply(assumption)
-apply(simp add: foo.eq_iff)
+apply(clarify)
+apply(simp (no_asm) add: foo.eq_iff)
+apply(perm_simp)
+apply(assumption)
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)