--- a/Nominal/Fv.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -154,16 +154,6 @@
 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) =
@@ -266,9 +256,8 @@
     "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 all_bns) bns;
+  val rel_bns = filter (fn (bn, _, _) => bn mem nr_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, _) =>
@@ -307,21 +296,15 @@
             @{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_compound_binder arg_no) bindcs of
-          SOME (f, is_rec) =>
+        case get_first (find_nonrec_binder arg_no) bindcs of
+          SOME f =>
             (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
-                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
+                SOME fv_bn => fv_bn $ x
               | NONE => error "bn specified in a non-rec binding but not in bn list")
         | NONE =>
             let