# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268169010 -3600
# Node ID 09899b909772a3bc5aae9d0a9f4fc8bfaff5860e
# Parent  dab8d99b37c1ef6b6d68b7327e3a266fea8f1127# Parent  5bb0149329ee2404e04a0e4b635c23f4d72892a9
merged

diff -r dab8d99b37c1 -r 09899b909772 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 09 22:08:38 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 09 22:10:10 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
 *)