# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268908630 -3600
# Node ID a9cb6a51efc37fcb2c480640253cae20055d2370
# Parent  883b38196dba4609b2b9872bddee2319ff4b5407# Parent  936587f6952e5e0880a48cb7f902ae099d23f615
merge

diff -r 936587f6952e -r a9cb6a51efc3 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 18 11:33:56 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 11:37:10 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
 *)