diff -r 42b7abf779ec -r 0c843fcb1d7b Nominal/Fv.thy
--- a/Nominal/Fv.thy	Mon Mar 08 10:08:31 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 10:33:55 2010 +0100
@@ -2,15 +2,15 @@
 imports "Nominal2_Atoms" "Abs" "Perm" "Rsp"
 begin
 
-(* TODO: update the comment *)
-(* Bindings are given as a list which has a length being equal
-   to the length of the number of constructors.
+(* Bindings are a list of lists of lists of triples.
 
-   Each element is a list whose length is equal to the number
-   of arguents.
+   The first list represents the datatypes defined.
+   The second list represents the constructors.
+   The internal list is a list of all the bndings that
+   concern the constructor.
 
-   Every element specifies bindings of this argument given as
-   a tuple: function, bound argument.
+   Every triple consists of a function, the binding and
+   the body.
 
   Eg:
 nominal_datatype
@@ -22,12 +22,12 @@
 yields:
 [
  [],
- [[], [], [(NONE, 0)]],
- [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
+ [(NONE, 0, 2)],
+ [(SOME (Const f), 0, 2), (Some (Const g), 1, 2)]]
 
-A SOME binding has to have a function returning an atom set,
-and a NONE binding has to be on an argument that is an atom
-or an atom set.
+A SOME binding has to have a function which takes an appropriate
+argument and returns an atom set. A NONE binding has to be on an
+argument that is an atom or an atom set.
 
 How the procedure works:
   For each of the defined datatypes,
@@ -53,8 +53,12 @@
     (* TODO: This one is not implemented *)
     For other arguments it should be an appropriate fv function stored
       in the database.
+
+  For every argument that is a binding, we add a the same binding in its
+  body.
 *)
 
+(* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []
   | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys
@@ -62,6 +66,8 @@
   | map2i _ _ _ = raise UnequalLengths;
 *}
 
+(* Finds bindings with the same function and binding, and gathers all
+   bodys for such pairs *)
 ML {*
 fun gather_binds binds =
 let
@@ -261,7 +267,7 @@
 
 (* to be given by the user *)
 
-primrec 
+primrec
   bv1
 where
   "bv1 (BUnit) = {}"