--- a/Nominal/Parser.thy	Mon Mar 15 14:32:05 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 15 17:42:17 2010 +0100
@@ -319,8 +319,8 @@
   val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
-  val fv_ts_loc_nobn = List.take (fv_ts_loc, length perms)
-  val fv_ts_nobn = List.take (fv_ts, length perms)
+  val (fv_ts_loc_nobn, fv_ts_loc_bn) = chop (length perms) fv_ts_loc;
+  val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
   val alpha_induct_loc = #induct alpha
@@ -346,7 +346,9 @@
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
-  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
+  val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
+  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;
   val alpha_equivp_loc = 

--- a/Nominal/Test.thy	Mon Mar 15 14:32:05 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 17:42:17 2010 +0100
@@ -7,6 +7,7 @@
 atom_decl name
 
 ML {* val cheat_alpha_eqvt = ref false *}
+ML {* val cheat_fv_eqvt = ref false *}
 
 nominal_datatype lam =
   VAR "name"