diff -r 8ffede2c8ce9 -r e32ec6e61154 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon May 03 12:24:27 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 13:42:44 2010 +0200
@@ -272,9 +272,11 @@
 end
 *}
 
-ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *}
-ML {* val cheat_equivp = Unsynchronized.ref true *}
-ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_equivp = Unsynchronized.ref false *}
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
+ML {* val cheat_supp_eq = Unsynchronized.ref false *}
 
 text {* 
   nominal_datatype2 does the following things in order:
@@ -443,9 +445,11 @@
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-(*  val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;*)
+  fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
+    else
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-        (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
+    alpha_bn_rsp_tac) alpha_ts_bn lthy11
   fun const_rsp_tac _ =
     let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
       in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
@@ -493,7 +497,8 @@
   val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
-  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
+  val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff;
+  val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff_simp) lthy17;
   val q_dis = map (lift_thm qtys lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
   val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
@@ -510,9 +515,10 @@
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
   val _ = warning "Support Equations";
-  val q_eq_iff_simp = map (fn x => @{thm simp_thms(6)} OF [x] handle THM _ => x) q_eq_iff;
-  (*supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1*)
-  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => Skip_Proof.cheat_tac thy)) handle _ => [];
+  fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
+    supp_eq_tac q_induct q_fv q_perm q_eq_iff_simp lthy22 1;
+  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
+    let val _ = warning ("Support eqs failed") in [] end;
   val lthy23 = note_suffix "supp" q_supp lthy22;
 in
   (0, lthy23)