--- a/Nominal/Parser.thy	Mon Mar 22 17:21:27 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 22 18:29:29 2010 +0100
@@ -337,7 +337,7 @@
   val _ = tracing "Proving equivalence";
   val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
   val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
     else build_equivps alpha_ts reflps alpha_induct