--- a/Quot/Examples/Terms.thy	Thu Jan 14 12:17:39 2010 +0100
+++ b/Quot/Examples/Terms.thy	Thu Jan 14 12:23:59 2010 +0100
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-(* lets with binding patterns *)
+(*** lets with binding patterns ***)
 datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"
@@ -15,7 +15,15 @@
 | BVr "name"
 | BPr "bp" "bp"
 
-(* lets with single assignments *)
+(* to be given by the user *)
+fun 
+  bv1
+where
+  "bv1 (BUnit) = {}"
+| "bv1 (BVr x) = {x}"
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
+
+(*** lets with single assignments ***)
 datatype trm2 =
   Vr2 "name"
 | Ap2 "trm2" "trm2"
@@ -24,8 +32,14 @@
 and assign =
   As "name" "trm2"
 
+(* to be given by the user *)
+fun 
+  bv2
+where
+  "bv2 (As x t) = {x}"
 
-(* lets with many assignments *)
+
+(*** lets with many assignments ***)
 datatype trm3 =
   Vr3 "name"
 | Ap3 "trm3" "trm3"
@@ -35,3 +49,11 @@
   ANil
 | ACons "name" "trm3" "assigns"
 
+(* to be given by the user *)
+fun 
+  bv3
+where
+  "bv3 ANil = {}"
+| "bv3 (ACons x t as) = {x} \<union> (bv3 as)"
+
+end
\ No newline at end of file