diff -r fb201e383f1b -r da575186d492 Nominal/Ex/LetFun.thy
--- a/Nominal/Ex/LetFun.thy	Tue Feb 19 05:38:46 2013 +0000
+++ b/Nominal/Ex/LetFun.thy	Tue Feb 19 06:58:14 2013 +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