--- 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