diff -r 5111dadd1162 -r f7ec6f7b152e Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Thu May 13 19:06:54 2010 +0100
+++ b/Nominal/NewFv.thy	Fri May 14 10:21:14 2010 +0200
@@ -133,10 +133,9 @@
 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
 let
   val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
-  val bound_vars =
-    case binds of
-      [(SOME bn, i)] => set (bn $ nth args i)
-    | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds));
+  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)] =>