--- a/Nominal/Ex/SingleLet.thy	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy	Mon Sep 27 09:51:15 2010 -0400
@@ -21,7 +21,6 @@
 where
   "bn (As x y t) = [atom x]"
 
-
 thm single_let.distinct
 thm single_let.induct
 thm single_let.inducts
@@ -37,9 +36,6 @@
 thm single_let.supp
 thm single_let.size
 
-thm single_let.supp(1-2)
-thm single_let.fv_defs[simplified single_let.supp(1-2)]
-
 
 end