--- a/Nominal/Ex/CPS/Lt.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Mon May 19 16:45:46 2014 +0100
@@ -33,7 +33,7 @@
   apply(simp add: perm_supp_eq fresh_star_Pair)
 done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
   shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M"
@@ -54,7 +54,7 @@
   by (auto)
      (erule lt.exhaust, auto)
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure size") (simp_all)
 
 inductive