--- a/Nominal/Ex/SFT/Lambda.thy	Fri Jul 22 11:52:12 2011 +0100
+++ b/Nominal/Ex/SFT/Lambda.thy	Sun Jul 24 07:54:54 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"