--- a/Nominal/Ex/Classical.thy	Wed May 12 16:18:04 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Wed May 12 16:32:44 2010 +0200
@@ -12,7 +12,6 @@
 atom_decl name
 atom_decl coname
 
-ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = cheat_equivp := true *}
 ML {* val _ = cheat_fv_rsp := true *}
 

--- a/Nominal/Ex/ExPS3.thy	Wed May 12 16:18:04 2010 +0200
+++ b/Nominal/Ex/ExPS3.thy	Wed May 12 16:32:44 2010 +0200
@@ -6,7 +6,6 @@
 
 atom_decl name
 
-ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = cheat_equivp := true *}
 ML {* val _ = cheat_alpha_bn_rsp := true *}
 

--- a/Nominal/NewParser.thy	Wed May 12 16:18:04 2010 +0200
+++ b/Nominal/NewParser.thy	Wed May 12 16:32:44 2010 +0200
@@ -436,23 +436,20 @@
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
-  fun alpha_eqvt_tac' _ =
-    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
-  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
+  val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
   val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
+    if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
     else build_equivps alpha_ts reflps alpha_induct
-      inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6;
+      inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6a;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>