--- a/Nominal/Fv.thy	Tue Mar 09 17:25:35 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 09 21:22:22 2010 +0100
@@ -156,13 +156,13 @@
 
 (* We assume no bindings in the type on which bn is defined *)
 ML {*
-fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bn) =
+fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
 let
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
   val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp));
-  fun fv_bn_constr (cname, dts) =
+  fun fv_bn_constr (cname, dts) args_in_bn =
   let
     val Ts = map (typ_of_dtyp descr sorts) dts;
     val names = Datatype_Prop.make_tnames Ts;
@@ -187,7 +187,7 @@
       (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos))))
   end;
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
-  val eqs = map fv_bn_constr constrs
+  val eqs = map2i fv_bn_constr constrs args_in_bns
 in
   ((bn, fvbn), (fvbn_name, eqs))
 end
@@ -352,7 +352,7 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
-  [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [0])] *}
+  [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
 print_theorems
 *)