diff -r 92f40c13d581 -r 727e0edad284 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Thu Apr 29 12:11:44 2010 +0200
+++ b/Nominal/NewFv.thy	Thu Apr 29 13:19:12 2010 +0200
@@ -102,8 +102,8 @@
     case binds of
       [(SOME bn, i)] =>
         if i mem bodys
-        then ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
-        else noatoms
+        then noatoms
+        else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
     | _ => noatoms
 in
   mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]