diff -r 4e5a7b606eab -r 08bbde090a17 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Fri Jun 11 03:02:42 2010 +0200
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 11]]
+declare [[STEPS = 12]]
 
 nominal_datatype tkind =
   KStar
@@ -85,6 +85,7 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
+
 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