--- a/Nominal/Ex/Local_Contexts.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/Local_Contexts.thy	Mon May 19 16:45:46 2014 +0100
@@ -55,7 +55,7 @@
 apply (metis Pair_eqvt perm_supp_eq)
 done
 
-termination (in name_subst) (eqvt) by lexicographic_order
+nominal_termination (in name_subst) (eqvt) by lexicographic_order
 
 inductive (in name_subst) beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<longrightarrow>\<^sub>\<beta>" 90)
 where