--- a/Nominal/Ex/Let.thy	Wed Sep 29 09:47:26 2010 -0400
+++ b/Nominal/Ex/Let.thy	Wed Sep 29 16:49:13 2010 -0400
@@ -74,23 +74,22 @@
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
-  assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P"
-  and     "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>assn trm ca. \<lbrakk>set (bn assn) \<sharp>* ca; c = ca; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
+  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
+  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
+  and     "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
   shows "P"
 apply(rule_tac y="y" in trm_assn.exhaust(1))
 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 trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(3))
 apply(perm_simp)
 apply(assumption)
-apply(rule refl)
 apply(drule supp_perm_eq[symmetric])
 apply(simp)
 apply(rule at_set_avoiding2)
@@ -98,13 +97,12 @@
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: trm_assn.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* c \<and> supp ([bn assn]lst.trm) \<sharp>* q")
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
-apply(rule assms(4))
+apply(rule_tac assms(4))
 apply(simp add: set_eqvt)
 apply(simp add: tt)
-apply(rule refl)
 apply(simp)
 apply(simp add: trm_assn.eq_iff)
 apply(drule supp_perm_eq[symmetric])
@@ -119,14 +117,14 @@
 
 
 lemma strong_exhaust2:
-  assumes "\<And>ca. \<lbrakk>c = ca; as = ANil\<rbrakk> \<Longrightarrow> P" 
-  and     "\<And>x t assn ca. \<lbrakk>c = ca; as = ACons x t assn\<rbrakk> \<Longrightarrow> P" 
+  assumes "as = ANil \<Longrightarrow> P" 
+  and     "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" 
   shows "P"
 apply(rule_tac y="as" in trm_assn.exhaust(2))
 apply(rule assms(1))
-apply(auto)[2]
+apply(assumption)
 apply(rule assms(2))
-apply(auto)[2]
+apply(assumption)+
 done
 
 
@@ -152,8 +150,7 @@
 apply(blast)
 apply(blast)
 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
-apply(auto)[1]
-apply(simp_all add: trm_assn.size)[7]
+apply(simp_all add: trm_assn.size)
 done
 
 text {* *}