--- a/Nominal/Ex/SubstNoFcb.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/SubstNoFcb.thy	Mon May 19 16:45:46 2014 +0100
@@ -31,7 +31,7 @@
   apply (metis (no_types) Pair_inject lam.distinct)+
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma lam_rec_cong[fundef_cong]:
   " (\<And>v. l = Var v \<Longrightarrow> fv v = fv' v) \<Longrightarrow>
@@ -58,7 +58,7 @@
 apply (rule, perm_simp, rule, rule)
 by pat_completeness auto
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma fresh_fun_eqvt_app3:
   assumes e: "eqvt f"