--- a/Nominal/Fv.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -154,6 +154,16 @@
 end
 *}
 
+ML {*
+fun all_binds l =
+let
+  fun is_non_rec (SOME (f, _), _, _) = SOME f
+    | is_non_rec _ = NONE
+in
+  distinct (op =) (map_filter is_non_rec (flat (flat l)))
+end
+*}
+
 (* 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_bns) =
@@ -244,8 +254,6 @@
   length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1
 *}
 
-ML {* fn x => split_list(flat x) *}
-ML {* fn x => apsnd flat (split_list (map split_list x)) *}
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
@@ -257,8 +265,9 @@
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
+  val all_bns = all_binds bindsall;
   val nr_bns = non_rec_binds bindsall;
-  val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
+  val rel_bns = filter (fn (bn, _, _) => bn mem all_bns) bns;
   val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
@@ -297,13 +306,21 @@
             @{term "{} :: atom set"}
         | fv_bind args (SOME (f, _), i, _) = f $ (nth args i);
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
-      fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE
-        | find_nonrec_binder _ _ = NONE
+      fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE
+        | find_compound_binder _ _ = NONE
       fun fv_arg ((dt, x), arg_no) =
-        case get_first (find_nonrec_binder arg_no) bindcs of
-          SOME f =>
+        case get_first (find_compound_binder arg_no) bindcs of
+          SOME (f, is_rec) =>
             (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
-                SOME fv_bn => fv_bn $ x
+                SOME fv_bn =>
+                  if is_rec then
+                    let
+                      val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
+                      val sub = fv_binds args relevant
+                    in
+                      mk_diff (fv_bn $ x) sub
+                    end
+                  else fv_bn $ x
               | NONE => error "bn specified in a non-rec binding but not in bn list")
         | NONE =>
             let
@@ -312,7 +329,7 @@
                 if ((is_atom thy) o fastype_of) x then mk_single_atom x else
                 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else
                 (* TODO we do not know what to do with non-atomizable things *)
-                @{term "{} :: atom set"}
+                @{term "{} :: atom set"};
               (* If i = j then we generate it only once *)
               val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
               val sub = fv_binds args relevant