diff -r aa5059a00f41 -r 6fd3fc3254ee Nominal/Ex/LetFun.thy
--- a/Nominal/Ex/LetFun.thy	Wed Sep 21 17:16:11 2011 +0900
+++ b/Nominal/Ex/LetFun.thy	Wed Sep 21 10:23:06 2011 +0200
@@ -34,6 +34,7 @@
 thm exp_pat.eq_iff
 thm exp_pat.fv_bn_eqvt
 thm exp_pat.size_eqvt
+thm exp_pat.size
 thm exp_pat.supports
 thm exp_pat.fsupp
 thm exp_pat.supp