--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -14,7 +14,7 @@
 apply (rule, perm_simp, rule, rule)
 apply (simp_all add: fresh_Pair_elim)
 apply (rule_tac y="x" in lt.exhaust)
-apply (auto)
+apply (auto)[3]
 apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
 apply (simp_all add: fresh_at_base)[3]
 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
@@ -28,11 +28,16 @@
 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
 apply (case_tac "k = ka")
 apply simp
-apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
-apply (simp del: eqvts add: lt.fresh fresh_at_base)
+thm Abs1_eq_iff
+apply(subst Abs1_eq_iff)
+apply(auto)[2]
+apply(rule disjI2)
+apply(rule conjI)
+apply(simp)
+apply(rule conjI)
 apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff)
 apply (subst  flip_at_base_simps(2))
-apply simp
+apply(simp)
 apply (intro conjI refl)
 apply (rule flip_fresh_fresh[symmetric])
 apply (simp_all add: lt.fresh)
@@ -125,18 +130,15 @@
 apply (rename_tac M N u K)
 apply (subgoal_tac "Lam n (M+ $ n~ $ K) =  Lam u (M+ $ u~ $ K)")
 apply (simp only:)
-apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]
+apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1]
 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
 apply (simp only:)
-apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)
-apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")
-apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka")
-apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka")
+apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)
+apply(simp_all add: flip_def[symmetric])
 apply (case_tac "m = ma")
 apply simp_all
-apply rule
-apply (auto simp add: flip_fresh_fresh[symmetric])
-apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
+apply (case_tac "m = na")
+apply(simp_all add: flip_fresh_fresh)
 done
 
 termination (eqvt)
@@ -227,7 +229,7 @@
     have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
       using * d e by simp
     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
-      by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base)
+      by (rule evbeta')(simp_all add: * d e)
     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
       assume f: "isValue lt2"
       have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp