--- a/Nominal/nominal_dt_rawfuns.ML	Fri Sep 03 20:53:09 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Fri Sep 03 22:22:43 2010 +0800
@@ -151,7 +151,7 @@
 
 (** functions that construct the equations for fv and fv_bn **)
 
-fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
+fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) =
 let
   fun mk_fv_body fv_map args i = 
   let
@@ -163,21 +163,33 @@
     | SOME fv => fv $ arg
   end  
 
-  fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = 
+  fun mk_fv_binder lthy fv_bn_map args binders = 
   let
-    val arg = nth args i
+    fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"})
+      | bind_set _ args (SOME bn, i) = (bn $ (nth args i), 
+          if  member (op=) bodies i then @{term "{}::atom set"}  
+          else lookup fv_bn_map bn $ (nth args i))
+    fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"})
+      | bind_lst _ args (SOME bn, i) = (bn $ (nth args i),
+          if  member (op=) bodies i then @{term "[]::atom list"}  
+          else lookup fv_bn_map bn $ (nth args i)) 
+  
+    val (combine_fn, bind_fn) =
+      case bmode of
+        Lst => (fold_append, bind_lst) 
+      | Set => (fold_union, bind_set)
+      | Res => (fold_union, bind_set)
   in
-    case bn_option of
-      NONE => (setify lthy arg, @{term "{}::atom set"})
-    | SOME bn => (to_set (bn $ arg), 
-       if  member (op=) bodies i then @{term "{}::atom set"}  
-       else lookup fv_bn_map bn $ arg)
+    binders
+    |> map (bind_fn lthy args)
+    |> split_list
+    |> pairself combine_fn
   end  
 
   val t1 = map (mk_fv_body fv_map args) bodies
-  val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
+  val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders
 in 
-  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
+  mk_union (mk_diff (fold_union t1, to_set t2), to_set t3)
 end
 
 (* in case of fv_bn we have to treat the case special, where an