--- a/Quot/Nominal/Fv.thy	Wed Feb 17 10:12:01 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 10:20:26 2010 +0100
@@ -16,6 +16,23 @@
 
 ML {* dest_Type @{typ rlam} *}
 
+(* Bindings are given as a list which has a length being equal
+   to the length of the number of constructors. Each element
+   is a specification of all the bindings n this constructor.
+   The bindings are given as triples: function, bound argument,
+   and the argument in which it is bound.
+
+  Eg:
+nominal_datatype
+
+   C1
+ | C2 x y z bind x in z
+ | C3 x y z bind f x in y bind g y in z
+
+yields:
+[[], [(NONE, 0, 2)], [(SOME (Const f), 0, 1), (Some (Const g), 1, 2)]]
+*)
+
 ML {*
   val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam";
   val sorts = [];