# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266398426 -3600
# Node ID b9d02e0800e97f29e8518dfca8fd7da730c5be74
# Parent  5c1e16806901bb334e1c89b5a641edc159d7fcf1
Description of intended bindings.

diff -r 5c1e16806901 -r b9d02e0800e9 Quot/Nominal/Fv.thy
--- 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 = [];