diff -r 1e6160690546 -r 107c06267f33 Nominal/Ex/CoreHaskell.thy --- 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