--- a/Nominal/Ex/CoreHaskell.thy	Mon Jun 28 15:23:56 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Mon Jun 28 16:22:28 2010 +0100
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 15]]
+declare [[STEPS = 16]]
 
 nominal_datatype tkind =
   KStar
@@ -85,6 +85,10 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
+
+term TvsNil
+
+
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm