--- a/Nominal/Ex/Lambda.thy	Fri Aug 27 02:25:40 2010 +0000
+++ b/Nominal/Ex/Lambda.thy	Fri Aug 27 13:57:00 2010 +0800
@@ -17,6 +17,7 @@
 thm lam.bn_defs
 thm lam.perm_simps
 thm lam.eq_iff
+thm lam.eq_iff[folded alphas]
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt