--- a/Nominal/Ex/CoreHaskell.thy	Sun Aug 08 10:12:38 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Aug 11 16:21:24 2010 +0800
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 16]]
+declare [[STEPS = 17]]
 
 nominal_datatype tkind =
   KStar
@@ -85,6 +85,9 @@
 | "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