--- a/Nominal/Parser.thy	Thu Mar 25 17:30:46 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 25 20:12:57 2010 +0100
@@ -374,10 +374,10 @@
   (* Could be done nicer *)
   val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
   val _ = tracing "Proving respects";
+  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ =>
-       if !cheat_bn_rsp then (Skip_Proof.cheat_tac thy) else
-       fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 1)) bns lthy8;
+       resolve_tac bns_rsp_pre' 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
     else fvbv_rsp_tac alpha_induct fv_def lthy8 1;