diff -r 604c4cffc5b9 -r c3dca6e600c8 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Sat Mar 20 08:56:07 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 20 09:27:28 2010 +0100
@@ -267,7 +267,7 @@
 
 (* These 2 are critical, we don't know how to do it in term5 *)
 ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
-ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *}
 
 ML {* val cheat_equivp = Unsynchronized.ref true *}
 
@@ -363,10 +363,13 @@
   val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-  fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
-    else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1
-  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
+  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_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    alpha_bn_rsp_tac) 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;