diff -r e12ebfa745f6 -r 883b38196dba Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 18 11:29:12 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 11:36:03 2010 +0100
@@ -54,7 +54,9 @@
 
    An fv for a constructor is a union of values for the arguments.
 
-   For an argument x that bound in a non-recursive binding
+   For an argument that is bound in a shallow binding we return empty.
+
+   For an argument x that bound in a non-recursive deep binding
    we return: fv_bn x.
 
    Otherwise we return the free variables of the argument minus the
@@ -70,8 +72,6 @@
    involve the given argument. For a paricular binding:
 
    - for a binding function bn: bn x
-   - for an atom: {atom x}
-   - for atom set: atom ` x
    - for a recursive argument of type ty': fv_fy' x
    - for nominal datatype ty' return: fv_ty' x
 *)