diff -r 4b4742aa43f2 -r 11f6a561eb4b Nominal/Ex/LetFun.thy
--- 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