--- a/Quot/Nominal/Terms.thy	Wed Feb 10 11:53:15 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 10 12:30:26 2010 +0100
@@ -1113,6 +1113,29 @@
 
 
 
+(* example with a respectful bn function defined over the type itself *)
+datatype rtrm7 =
+  rVr7 "name"
+| rLm7 "name" "rtrm7"
+| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
+
+primrec
+  rbv7
+where
+  "rbv7 (rVr7 n) = {atom n}"
+| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
+| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
+
+primrec
+  rfv_trm7
+where
+  "rfv_trm7 (rVr7 n) = {}"
+| "rfv_trm7 (rLm7 n t) = {atom n} \<union> (rfv_trm7 t)"
+| "rfv_trm7 (rLt7 l r) = (rfv_trm7 r) \<union> (rfv_trm7 l)"
+
+
+
+
 
 
 text {* type schemes *}