--- a/Nominal/NewParser.thy	Tue Jun 22 18:07:53 2010 +0100
+++ b/Nominal/NewParser.thy	Wed Jun 23 06:45:03 2010 +0100
@@ -291,21 +291,7 @@
 *}
 
 
-lemma equivp_hack: "equivp x"
-sorry
-ML {*
-fun equivp_hack ctxt rel =
-let
-  val thy = ProofContext.theory_of ctxt
-  val ty = domain_type (fastype_of rel)
-  val cty = ctyp_of thy ty
-  val ct = cterm_of thy rel
-in
-  Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
-end
-*}
 
-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 *}
@@ -463,15 +449,10 @@
     if get_STEPS lthy > 14
     then true else raise TEST lthy4
 
-  val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy4) alpha_trms
-    else build_equivps alpha_trms alpha_refl_thms alpha_induct
-      inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4;
-
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp_thms lthy4;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
@@ -504,7 +485,7 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   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_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms 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]
     alpha_bn_rsp_tac) alpha_bn_trms lthy11
   fun const_rsp_tac _ =