--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Jul 11 23:42:52 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Jul 12 03:12:32 2011 +0900
@@ -1,9 +1,6 @@
 header {* CPS transformation of Danvy and Filinski *}
 theory CPS3_DanvyFilinski imports Lt begin
 
-lemma TODO: "eqvt_at f a \<Longrightarrow> eqvt_at f (p \<bullet> a)"
-  sorry
-
 nominal_primrec
   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
 and
@@ -104,8 +101,7 @@
   apply (case_tac "c = xa")
   apply simp_all[2]
   apply (rotate_tac 1)
-  apply (drule TODO)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec)
+  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
   apply (simp add: swap_fresh_fresh)
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")
@@ -189,8 +185,7 @@
   apply (case_tac "c = xa")
   apply simp_all[2]
   apply (rotate_tac 1)
-  apply (drule TODO)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec)
+  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
   apply (simp add: swap_fresh_fresh)
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")