diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy	Mon May 10 15:45:04 2010 +0200
@@ -7,6 +7,9 @@
 
 atom_decl name
 
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -30,6 +33,11 @@
 thm trm_lts.supp
 thm trm_lts.fv[simplified trm_lts.supp]
 
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
 (* why is this not in HOL simpset? *)
 lemma set_sub: "{a, b} - {b} = {a} - {b}"
 by auto