--- a/Nominal/Ex/Lambda.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Lambda.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -661,12 +661,9 @@
   apply (case_tac a rule: lam.exhaust)
   using [[simproc del: alpha_lst]]
   apply simp_all[3]
-  apply blast
   apply (case_tac b)
   apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
   apply simp_all[3]
-  apply blast
-  apply blast
   apply (simp add: Abs1_eq_iff fresh_star_def)
   using [[simproc del: alpha_lst]]
   apply(simp_all)
@@ -713,8 +710,6 @@
 apply (rule_tac y="a" in lam.exhaust)
 using [[simproc del: alpha_lst]]
 apply simp_all
-apply blast
-apply blast
 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)
 apply blast
 apply clarify