diff -r 0d95e19e4f93 -r d8a6b424f80a Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Mon Jul 11 23:42:52 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Tue Jul 12 03:12:32 2011 +0900
@@ -70,12 +70,11 @@
   apply (erule fresh_eqvt_at)
   apply (simp add: supp_Inr finite_supp)
   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only: )
+  apply (simp only:)
+  apply (simp (no_asm))
   apply (erule_tac c="a" in Abs_lst1_fcb2')
   apply (simp add: Abs_fresh_iff lt.fresh)
   apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base)
-  apply (subgoal_tac "p \<bullet> CPS1_CPS2_sumC (Inr (M, a~)) = CPS1_CPS2_sumC (p \<bullet> (Inr (M, a~)))")
-  apply (simp add: perm_supp_eq fresh_star_def lt.fresh)
   oops
 
 end