diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon May 19 16:45:46 2014 +0100
@@ -63,7 +63,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 (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
 
@@ -89,7 +89,7 @@
   apply (simp add: Abs1_eq_iff CPS.eqvt)
   by blast
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure size") (simp_all)
 
 lemma convert_supp[simp]:
@@ -143,7 +143,7 @@
 apply(simp_all add: flip_fresh_fresh)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
 
 section{* lemma related to Kapply *}