diff -r 118a0ca16381 -r 387fcbd33820 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Wed Jun 02 11:37:51 2010 +0200
@@ -2,15 +2,14 @@
 imports "../NewParser"
 begin
 
-(* core haskell *)
-
-(* at the moment it is hard coded that shallow binders 
-   need to use bind_set *)
+(* Core Haskell *)
 
 atom_decl var
 atom_decl cvar
 atom_decl tvar
 
+declare [[STEPS = 4]]
+
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -85,6 +84,8 @@
 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
 | "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]