--- a/Nominal/NewFv.thy	Fri May 14 10:28:42 2010 +0200
+++ b/Nominal/NewFv.thy	Fri May 14 15:37:23 2010 +0200
@@ -136,15 +136,13 @@
   fun bound_var (SOME bn, i) = set (bn $ nth args i)
     | bound_var (NONE, i) = fv_body thy dts args fv_frees false i
   val bound_vars = mk_union (map bound_var binds);
-  val non_rec_vars =
-    case binds of
-      [(SOME bn, i)] =>
-        if member (op =) bodys i
-        then noatoms
-        else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
-    | _ => noatoms
+  fun non_rec_var (SOME bn, i) =
+      if member (op =) bodys i
+      then noatoms
+      else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
+    | non_rec_var (NONE, _) = noatoms
 in
-  mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]
+  mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds))
 end
 *}