--- a/Nominal/Parser.thy	Mon Mar 22 10:15:46 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 22 14:07:07 2010 +0100
@@ -265,13 +265,11 @@
 end
 *}
 
-(* These 2 are critical, we don't know how to do it in term5 *)
-ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *}
-
 ML {* val cheat_equivp = Unsynchronized.ref true *}
 
-(* These 2 are not needed any more *)
+(* These 3 are not needed any more *)
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 
@@ -332,7 +330,8 @@
     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 (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 alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
@@ -356,11 +355,15 @@
   val _ = tracing "Proving respects";
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t]
-      (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8;
+      (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs lthy8 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 1;
-  val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
+    else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
+  val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
+  val (fv_rsp_pre, lthy10) = fold_map
+    (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv]
+    (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9;
+  val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11;