--- a/Nominal/Ex/SingleLet.thy	Mon May 03 15:13:15 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Mon May 03 15:36:47 2010 +0200
@@ -4,8 +4,6 @@
 
 atom_decl name
 
-ML {* val _ = cheat_alpha_eqvt := true *}
-
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
@@ -18,7 +16,6 @@
 where
   "bn (As x t) = {atom x}"
 
-thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff
@@ -30,11 +27,12 @@
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
 thm trm_assg.fv[simplified trm_assg.supp(1-2)]
 
+(*
 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
 declare permute_trm_raw_permute_assg_raw.simps[eqvt]
 declare alpha_gen_eqvt[eqvt]
 equivariance alpha_trm_raw
-
+*)
 
 end