--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -22,11 +22,13 @@
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
   apply (auto simp add: fresh_star_def)
   apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff)
+  apply (simp_all add: Abs_fresh_iff)[2]
   apply (erule fresh_eqvt_at)
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: swap_fresh_fresh)
+  apply(simp)
   done
 
 termination (eqvt) by lexicographic_order
@@ -49,7 +51,8 @@
   apply (erule fresh_eqvt_at)
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: swap_fresh_fresh)
   done
 
 termination (eqvt) by lexicographic_order