diff -r 01ae4a87c7c3 -r 139b257e10d2 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 09 12:22:00 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 09 14:32:37 2010 +0100
@@ -319,8 +319,8 @@
 datatype rtrm2 =
   rVr2 "name"
 | rAp2 "rtrm2" "rtrm2"
-| rLm2 "name" "rtrm2"
-| rLt2 "rassign" "rtrm2"
+| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
+| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
 and rassign =
   rAs "name" "rtrm2"
 
@@ -411,8 +411,8 @@
 datatype trm3 =
   Vr3 "name"
 | Ap3 "trm3" "trm3"
-| Lm3 "name" "trm3"
-| Lt3 "assigns" "trm3"
+| Lm3 "name" "trm3" --"bind (name) in (trm3)"
+| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
 and assigns =
   ANil
 | ACons "name" "trm3" "assigns"
@@ -506,7 +506,7 @@
 datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
-| Lm4 "name" "trm4"
+| Lm4 "name" "trm4"  --"bind (name) in (trm)"
 
 thm trm4.recs
 
@@ -596,7 +596,7 @@
 datatype rtrm5 =
   rVr5 "name"
 | rAp5 "rtrm5" "rtrm5"
-| rLt5 "rlts" "rtrm5"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
 and rlts =
   rLnil
 | rLcons "name" "rtrm5" "rlts"