diff -r 6b496f69f76c -r a27215ab674e Nominal/Ex/LetRecB.thy
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:45:30 2011 +0900
+++ b/Nominal/Ex/LetRecB.thy	Wed Jun 29 00:48:50 2011 +0100
@@ -181,6 +181,11 @@
   apply (simp add: eqvt_at_def)
   apply (simp add: eqvt_at_def)
 --""
+  apply(simp_all add: eqvt_def inj_on_def)
+  apply(perm_simp)
+  apply(simp)
+  apply(perm_simp)
+  apply(simp)
   done
 
 termination by lexicographic_order