--- a/Nominal/Ex/Let.thy	Wed Dec 22 09:13:25 2010 +0000
+++ b/Nominal/Ex/Let.thy	Wed Dec 22 10:32:01 2010 +0000
@@ -30,39 +30,6 @@
 thm trm_assn.exhaust
 thm trm_assn.strong_exhaust
 
-lemma strong_exhaust1:
-  fixes c::"'a::fs"
-  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.strong_exhaust(1))
-apply(rule assms(1))
-apply(assumption)
-apply(rule assms(2))
-apply(assumption)
-apply(rule assms(3))
-apply(assumption)
-apply(assumption)
-apply(rule assms(4))
-apply(assumption)
-apply(assumption)
-sorry
-
-
-lemma strong_exhaust2:
-  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(assumption)
-apply(rule assms(2))
-apply(assumption)+
-done
-
-
 lemma 
   fixes t::trm
   and   as::assn
@@ -76,12 +43,12 @@
   shows "P1 c t" "P2 c as"
 using assms
 apply(induction_schema)
-apply(rule_tac y="t" in strong_exhaust1)
+apply(rule_tac y="t" in trm_assn.strong_exhaust(1))
 apply(blast)
 apply(blast)
 apply(blast)
 apply(blast)
-apply(rule_tac as="as" in strong_exhaust2)
+apply(rule_tac ya="as" in trm_assn.strong_exhaust(2))
 apply(blast)
 apply(blast)
 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")