--- a/Nominal/Parser.thy	Sat Mar 20 04:51:26 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 20 08:04:59 2010 +0100
@@ -332,9 +332,11 @@
     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
   val _ = tracing "Proving equivalence";
+  val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
-    else build_equivps alpha_ts induct alpha_induct
+    else build_equivps alpha_ts reflps alpha_induct
       inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;