--- a/Nominal/Ex/CoreHaskell.thy	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Sun Aug 15 11:03:13 2010 +0800
@@ -85,8 +85,7 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-thm alpha_sym_thms
-thm funs_rsp
+
 thm distinct
 
 term TvsNil