Nominal/nominal_dt_rawfuns.ML
changeset 2375 e163fd99de44
parent 2321 e9b0728061a8
child 2384 841b7e34e70a
--- a/Nominal/nominal_dt_rawfuns.ML	Mon Jul 19 14:20:23 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon Jul 19 16:59:43 2010 +0100
@@ -35,6 +35,11 @@
 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
 struct
 
+(* term              - is constant of the bn-function 
+   int               - is datatype number over which the bn-function is defined
+   int * term option - is number of the corresponding argument with possibly
+                       recursive call with bn-function term 
+*)  
 type bn_info = (term * int * (int * term option) list list) list
 
 datatype bmode = Lst | Res | Set