diff -r fd85f4921654 -r e8b9c0ebf5dd Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Fri Jul 23 16:42:47 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Sun Jul 25 22:42:21 2010 +0200
@@ -34,18 +34,19 @@
   and   "alpha_assg_raw x2 y2 \<Longrightarrow> alpha_bn_raw x2 y2"
   and   "alpha_bn_raw x3 y3 \<Longrightarrow> True"
 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all)
+apply(rule TrueI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(assumption)
-done
+sorry
 
 lemma a2:
   shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1"
   and   "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
   and   "alpha_bn_raw x3 y3 \<Longrightarrow>  fv_bn_raw x3 = fv_bn_raw y3"
 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all add: alphas a1 prod_alpha_def)
-apply(auto)
+apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
+apply(simp_all only: alphas prod_alpha_def)
+apply(auto)[1]
+apply(auto simp add: prod_alpha_def)
 done
 
 lemma [quot_respect]: