diff -r 5e74bd87bcda -r 9bcf02a6eea9 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Wed Dec 21 15:47:42 2011 +0900
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Wed Dec 21 17:05:00 2011 +0900
@@ -17,12 +17,12 @@
 apply (auto)
 apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
 apply (simp_all add: fresh_at_base)[3]
-apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-apply (simp add: fresh_Pair_elim fresh_at_base)[2]
 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)
 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh)
 apply (simp add: fresh_Pair_elim fresh_at_base)
+apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+apply (simp add: fresh_Pair_elim fresh_at_base)[2]
 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
 --"-"
 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
@@ -30,7 +30,7 @@
 apply simp
 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
 apply (simp del: eqvts add: lt.fresh fresh_at_base)
-apply (simp only: lt.perm_simps(1) lt.perm_simps(3) flip_def[symmetric] lt.eq_iff(3))
+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 (intro conjI refl)