diff -r 84afb941df53 -r d1038e67923a Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -322,7 +322,7 @@
   apply(simp_all add: ty2.distinct)
   done
 
-termination
+termination (eqvt)
   by lexicographic_order
 
 lemma subst_eqvt[eqvt]: