diff -r 84afb941df53 -r d1038e67923a Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -216,7 +216,7 @@
   apply(blast)
   done
 
-termination 
+termination (eqvt)
   by lexicographic_order
 
 nominal_primrec 
@@ -379,7 +379,7 @@
   apply(blast)
   done
 
-termination 
+termination (eqvt)
   by lexicographic_order
 
 lemma crename_name_eqvt[eqvt]: