--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Wed Dec 21 15:47:42 2011 +0900
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Wed Dec 21 17:05:00 2011 +0900
@@ -74,19 +74,20 @@
   apply (case_tac x)
   apply (rule_tac y="a" in lt.exhaust)
   apply auto
+  apply blast
   apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
   apply (simp add: Abs1_eq_iff)
   apply blast+
   apply (rule_tac y="b" in lt.exhaust)
   apply auto
-  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
-  apply (simp add: Abs1_eq_iff)
-  apply blast
   apply (rule_tac ?'a="name" in obtain_fresh)
   apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh)
   apply (simp add: fresh_Pair_elim)
   apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1]
   apply (simp_all add: fresh_Pair)[4]
+  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
+  apply (simp add: Abs1_eq_iff)
+  apply blast
 --""
   apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh)
   apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")