diff -r 097b25706436 -r d78c093aebeb Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 15 10:02:19 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 15 10:07:15 2010 +0100
@@ -279,6 +279,8 @@
 ML {* val cheat_fv_rsp = ref true *}
 ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
 
+ML {* val cheat_equivp = ref true *}
+
 (* Fixes for these 2 are known *)
 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *)
@@ -346,9 +348,10 @@
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
-  val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn
-(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
-    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
+  val alpha_equivp_loc = 
+    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
+    else build_equivps alpha_ts_loc induct alpha_induct_loc
+      inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;