--- a/Nominal/Test.thy	Fri Feb 26 18:21:39 2010 +0100
+++ b/Nominal/Test.thy	Fri Feb 26 18:38:25 2010 +0100
@@ -17,6 +17,8 @@
 
 typ lam_raw
 term VAR_raw
+term APP_raw
+term LET_raw
 term Test.BP_raw
 thm bi_raw.simps
 
@@ -172,7 +174,7 @@
 
 nominal_datatype foo8 =
   Foo0 "name"
-| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in foo
+| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
 and bar8 =
   Bar0 "name"
 | Bar1 "name" s::"name" b::"bar8" bind s in b
@@ -285,7 +287,7 @@
 
 nominal_datatype trm =
   Var var
-| LAM tv::tvar kind t::trm   bind v in t 
+| LAM tv::tvar kind t::trm   bind tv in t 
 | APP trm ty
 | Lam v::var ty t::trm       bind v in t
 | App trm trm