diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -155,8 +155,7 @@
 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
 
-termination
-  by (relation "measure size") (simp_all add: lt.size)
+termination (eqvt) by (relation "measure size") (simp_all)
 
 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
 
@@ -167,25 +166,6 @@
 lemma [simp]: "x \<sharp> M* = x \<sharp> M"
   unfolding fresh_def by simp
 
-(* Will be provided automatically by nominal_primrec *)
-lemma CPS_eqvt[eqvt]:
-  shows "p \<bullet> M* = (p \<bullet> M)*"
-  apply (induct M rule: lt.induct)
-  apply (rule_tac x="(name, p \<bullet> name, p)" and ?'a="name" in obtain_fresh)
-  apply simp
-  apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric])
-  apply (metis atom_eqvt flip_fresh_fresh fresh_perm atom_eq_iff fresh_at_base)
-  apply (rule_tac x="(name, lt, p \<bullet> name, p \<bullet> lt, p)" and ?'a="name" in obtain_fresh)
-  apply simp
-  apply (metis atom_eqvt fresh_perm atom_eq_iff)
-  apply (rule_tac x="(lt1, p \<bullet> lt1, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh)
-  apply (rule_tac x="(a, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh)
-  apply (rule_tac x="(a, aa, p)" and ?'a="name" in obtain_fresh)
-  apply (simp)
-  apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric])
-  apply (metis atom_eqvt fresh_perm atom_eq_iff)
-  done
-
 nominal_primrec
   convert:: "lt => lt" ("_+" [250] 250)
 where
@@ -197,11 +177,11 @@
   apply (erule lt.exhaust)
   apply (simp_all)
   apply blast
-  apply (simp add: Abs1_eq_iff CPS_eqvt)
+  apply (simp add: Abs1_eq_iff CPS.eqvt)
   by blast
 
-termination
-  by (relation "measure size") (simp_all add: lt.size)
+termination (eqvt)
+  by (relation "measure size") (simp_all)
 
 lemma convert_supp[simp]:
   shows "supp (M+) = supp M"
@@ -211,10 +191,6 @@
   shows "x \<sharp> (M+) = x \<sharp> M"
   unfolding fresh_def by simp
 
-lemma convert_eqvt[eqvt]:
-  shows "p \<bullet> (M+) = (p \<bullet> M)+"
-  by (nominal_induct M rule: lt.strong_induct, auto simp add: CPS_eqvt)
-
 lemma [simp]:
   shows "isValue (p \<bullet> (M::lt)) = isValue M"
   by (nominal_induct M rule: lt.strong_induct) auto
@@ -265,8 +241,8 @@
 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
 done
 
-termination
-  by (relation "measure (\<lambda>(t, _). size t)") (simp_all add: lt.size)
+termination (eqvt)
+  by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
 
 section{* lemma related to Kapply *}