diff -r f496e9f343b7 -r 1471f2974eb1 src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -52,11 +52,7 @@
 apply(drule_tac x="a" in meta_spec)
 apply(blast)
 done
-
-termination vsub
-proof
-  show "wf (measure (llam_size \<circ> fst))" by simp
-qed (auto)
+termination by (relation "measure (llam_size \<circ> fst)") auto
 
 lemma vsub_eqvt[eqvt]:
   fixes pi::"name prm"