--- a/Nominal/Ex/TypeSchemes1.thy	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Mon May 19 16:45:46 2014 +0100
@@ -89,7 +89,7 @@
   apply(simp_all)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma subst_id1:
@@ -161,7 +161,7 @@
   apply blast
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by (lexicographic_order)
 
 
@@ -301,7 +301,7 @@
 apply(simp)
 done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
   
 lemma better:
@@ -412,7 +412,7 @@
   apply(simp_all)
   done
 
-termination (eqvt)
+nominal_termination (eqvt)
   by lexicographic_order
 
 lemma tt: