--- a/Nominal/Ex/ExCoreHaskell.thy	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal/Ex/ExCoreHaskell.thy	Fri Apr 09 21:51:01 2010 +0200
@@ -5,6 +5,9 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
+(* this should not be a raw equivariant rule *)
+declare permute_pure[eqvt]
+
 
 atom_decl var
 atom_decl cvar
@@ -88,6 +91,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