diff -r db1b5cb89aa4 -r 0ecc775e5fce Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 06:43:09 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 08:42:10 2010 +0100
@@ -11,9 +11,9 @@
 and bp = 
   BP "name" "lam" 
 binder
-  bi::"bp \<Rightarrow> name set"
+  bi::"bp \<Rightarrow> atom set"
 where
-  "bi (BP x t) = {x}"
+  "bi (BP x t) = {atom x}"
 
 typ lam_raw
 term VAR_raw
@@ -21,6 +21,8 @@
 term LET_raw
 term Test.BP_raw
 thm bi_raw.simps
+thm permute_lam_raw_permute_bp_raw.simps
+thm alpha_lam_raw_alpha_bp_raw.intros
 
 print_theorems