--- a/Nominal/Ex/LetFun.thy	Sat Dec 17 17:03:01 2011 +0000
+++ b/Nominal/Ex/LetFun.thy	Sat Dec 17 17:08:47 2011 +0000
@@ -34,7 +34,6 @@
 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