--- a/Nominal/Ex/Lambda.thy	Wed Sep 29 09:47:26 2010 -0400
+++ b/Nominal/Ex/Lambda.thy	Wed Sep 29 16:49:13 2010 -0400
@@ -26,20 +26,19 @@
 
 lemma strong_exhaust:
   fixes c::"'a::fs"
-  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>lam1 lam2 ca. \<lbrakk>c = ca; y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>name lam ca. \<lbrakk>c = ca; atom name \<sharp> ca; y = Lam name lam\<rbrakk> \<Longrightarrow> P"
+  assumes "\<And>name. \<lbrakk>y = Var name\<rbrakk> \<Longrightarrow> P"
+  and     "\<And>lam1 lam2. \<lbrakk>y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>name lam. \<lbrakk>atom name \<sharp> c; y = Lam name lam\<rbrakk> \<Longrightarrow> P"
   shows "P"
 apply(rule_tac y="y" in lam.exhaust)
 apply(rule assms(1))
-apply(auto)[2]
+apply(assumption)
 apply(rule assms(2))
-apply(auto)[2]
+apply(assumption)
 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(3))
-apply(rule refl)
 apply(simp add: atom_eqvt)
 apply(clarify)
 apply(drule supp_perm_eq[symmetric])
@@ -64,10 +63,7 @@
 apply(blast)
 apply(blast)
 apply(relation "measure (\<lambda>(x,y). size y)")
-apply(auto)[1]
-apply(simp add: lam.size)
-apply(simp add: lam.size)
-apply(simp add: lam.size)
+apply(simp_all add: lam.size)
 done
 
 section {* Strong Induction Principles*}