--- a/Nominal/Ex/AuxNoFCB.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/AuxNoFCB.thy	Mon May 19 16:45:46 2014 +0100
@@ -15,7 +15,7 @@
   apply (rule, perm_simp, rule, rule)
   by pat_completeness auto
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 nominal_function lam2_rec where
   "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs"
@@ -74,7 +74,7 @@
   apply simp
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma lam_rec2_cong[fundef_cong]:
   "(\<And>s1 s2 s3 s4. l = App s1 s2 \<Longrightarrow> l2 = App s3 s4  \<Longrightarrow> faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \<Longrightarrow>
@@ -106,7 +106,7 @@
   apply (rule, perm_simp, rule, rule)
   by pat_completeness auto
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all
 
 lemma aux_simps[simp]:
@@ -233,7 +233,7 @@
   apply (simp add: flip_fresh_fresh flip_eqvt)
   done
 
-termination (eqvt) by lexicographic_order
+nominal_termination (eqvt) by lexicographic_order
 
 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs"
   apply (induct xs)