--- a/Nominal/Parser.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -286,12 +286,10 @@
 end
 *}
 
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_equivp = Unsynchronized.ref false *}
-ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
-ML {* val cheat_bn_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_const_rsp = Unsynchronized.ref false *}
-ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
 ML {* fun map_option _ NONE = NONE
         | map_option f (SOME x) = SOME (f x) *}
@@ -342,7 +340,7 @@
     (rel_distinct ~~ alpha_ts_nobn));
   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
-  val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
+  val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv_ts_nobn @ fv_ts_bn) lthy5
@@ -394,13 +392,9 @@
       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11
+  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11a;
   val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    (fn _ =>
-      if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
-      else
-        let val alpha_bn_rsp_pre = flat (map (prove_alpha_bn_rsp alpha_ts_nobn alpha_inducts exhausts
-        (alpha_eq_iff @ rel_dists @ rel_dists_bn) (alpha_equivp) lthy11a) (alpha_ts_bn ~~ bn_nos)) in
-        asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end)) alpha_ts_bn lthy11a
+        (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;