diff -r 05ccb61aa628 -r 847972b7b5ba Nominal/Ex/SFT/Lambda.thy
--- a/Nominal/Ex/SFT/Lambda.thy	Fri Aug 12 22:37:41 2011 +0200
+++ b/Nominal/Ex/SFT/Lambda.thy	Sun Aug 14 08:52:03 2011 +0200
@@ -10,7 +10,7 @@
 nominal_datatype lam =
   V "var"
 | Ap "lam" "lam" (infixl "\<cdot>" 98)
-| Lm x::"var" l::"lam"  bind x in l ("\<integral> _. _" [97, 97] 99)
+| Lm x::"var" l::"lam"  binds x in l ("\<integral> _. _" [97, 97] 99)
 
 nominal_primrec
   subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
@@ -48,13 +48,7 @@
     by (rule, perm_simp, rule)
 qed
 
-termination
-  by (relation "measure (\<lambda>(t,_,_). size t)")
-     (simp_all add: lam.size)
-
-lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
-  by (induct t x s rule: subst.induct) (simp_all)
+termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"