--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Wed Dec 21 15:47:42 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Wed Dec 21 17:05:00 2011 +0900
@@ -26,10 +26,9 @@
   apply (case_tac b)
   apply (rule_tac y="a" in lt.strong_exhaust)
   apply auto[3]
-  apply blast
+  apply blast+
   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 
   apply (simp add: fresh_at_base Abs1_eq_iff)
-  apply blast
 --"-"
   apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
   apply (simp only:)