diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/CPS/Lt.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -33,13 +33,7 @@
   apply (simp_all add: swap_fresh_fresh)
   done
 
-termination
-  by (relation "measure (\<lambda>(t, _, _). size t)")
-     (simp_all add: lt.size)
-
-lemma subst_eqvt[eqvt]:
-  shows "p\<bullet>(M[V/(x::name)]) = (p\<bullet>M)[(p\<bullet>V)/(p\<bullet>x)]"
-  by (induct M V x rule: subst.induct) (simp_all)
+termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
   shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M"
@@ -60,9 +54,8 @@
   by (perm_simp, auto)
      (erule lt.exhaust, auto)
 
-termination
-  by (relation "measure size")
-     (simp_all add: lt.size)
+termination (eqvt)
+  by (relation "measure size") (simp_all)
 
 lemma is_Value_eqvt[eqvt]:
   shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)"