1116 (* example with a respectful bn function defined over the type itself *)

  1117 datatype rtrm7 =

  1118   rVr7 "name"

  1119 | rLm7 "name" "rtrm7"

  1120 | rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"

  1121 

  1122 primrec

  1123   rbv7

  1124 where

  1125   "rbv7 (rVr7 n) = {atom n}"

  1126 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"

  1127 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"

  1128 

  1129 primrec

  1130   rfv_trm7

  1131 where

  1132   "rfv_trm7 (rVr7 n) = {}"

  1133 | "rfv_trm7 (rLm7 n t) = {atom n} \<union> (rfv_trm7 t)"

  1134 | "rfv_trm7 (rLt7 l r) = (rfv_trm7 r) \<union> (rfv_trm7 l)"

  1135 

  1136 

  1137 

  1138