diff -r 841b7e34e70a -r fe25a3ffeb14 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 27 14:37:59 2010 +0200
@@ -45,26 +45,7 @@
   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 only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps)
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps)
--- ""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc)
--- ""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
-apply(simp only: Un_insert_left Un_empty_right Un_empty_left)
--- ""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
---""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
-apply(simp (no_asm) only: simp_thms)
---""
-apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps)
-apply(simp only: Un_assoc set.simps append.simps)
+apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
 done
 
 lemma [quot_respect]: