--- a/Nominal/Parser.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -336,12 +336,6 @@
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
-  fun alpha_eqvt_tac' _ =
-    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4;
-  val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
-  val _ = map tracing (map PolyML.makestring alpha_eqvt)
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
@@ -351,6 +345,12 @@
   val lthy6 = lthy6a;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
+  fun alpha_eqvt_tac' _ =
+    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
+    else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6;
+  val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
+  val _ = map tracing (map PolyML.makestring alpha_eqvt)
   val alpha_equivp_loc = 
     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
     else build_equivps alpha_ts_loc induct alpha_induct_loc