diff -r a08eaea622d1 -r cfda1ec86a9e Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Mon Apr 19 09:25:43 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Mon Apr 19 09:25:55 2010 +0200
@@ -5,8 +5,8 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
-(* this should not be a raw equivariant rule *)
-(* we force it to be                         *)
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be       *)
 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
 thm eqvts
 (*declare permute_pure[eqvt]*)
@@ -679,5 +679,18 @@
   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 qed
 
+section {* test about equivariance for alpha *}
+
+thm eqvts
+thm eqvts_raw
+
+declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_tkind_raw
+
+thm eqvts
+thm eqvts_raw
+
 end