--- a/Nominal/Parser.thy	Mon Mar 22 15:27:01 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 22 17:21:27 2010 +0100
@@ -265,13 +265,13 @@
 end
 *}
 
-ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *}
 ML {* val cheat_equivp = Unsynchronized.ref true *}
 
-(* These 3 are not needed any more *)
+(* These 4 are not needed any more *)
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
 
 
 ML {*
@@ -300,6 +300,7 @@
   val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
+  val exhausts = map #exhaust dtinfos;
   val _ = tracing "Defining permutations, fv and alpha";
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
@@ -308,11 +309,15 @@
     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
   val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
-  val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
+  val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
   val bns = raw_bn_funs ~~ bn_nos;
+  val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
+    (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 _ = tracing "Proving equivariance";
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
@@ -368,11 +373,11 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11;
   fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1
-  fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x
   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 = 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))
   val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    alpha_bn_rsp_tac) 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;
@@ -411,8 +416,6 @@
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
-  val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
-    (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
   val q_dis = map (lift_thm lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
   val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;