--- a/Nominal/Test.thy	Wed Mar 10 12:53:44 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 10 13:10:00 2010 +0100
@@ -42,7 +42,7 @@
 term Test.BP_raw
 thm bi_raw.simps
 thm permute_lam_raw_permute_bp_raw.simps
-thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
+thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros[no_vars]
 thm fv_lam_raw_fv_bp_raw.simps[no_vars]
 (*thm lam_bp_induct
 thm lam_bp_perm
@@ -77,7 +77,7 @@
 *)
 
 
-thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
+thm alpha_trm'_raw_alpha_pat'_raw_alpha_f_raw.intros[no_vars]
 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
 thm f_raw.simps
 (*thm trm'_pat'_induct
@@ -167,7 +167,7 @@
 
 
 thm fv_trm2_raw_fv_assign_raw.simps[no_vars]
-thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars]
+thm alpha_trm2_raw_alpha_assign_raw_alpha_bv2_raw.intros[no_vars]
 
 
 
@@ -339,11 +339,11 @@
   "cbinders (Type t T) = {atom t}"
 | "cbinders (Dty t) = {atom t}"
 | "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"*)
+| "cbinders (Val v M) = {atom v}"
 | "Cbinders (Type1 t) = {atom t}"
 | "Cbinders (Type2 t T) = {atom t}"
 | "Cbinders (SStru x S) = {atom x}"
-| "Cbinders (SVal v T) = {atom v}"  
+| "Cbinders (SVal v T) = {atom v}"
 
 
 (* core haskell *)
@@ -424,18 +424,18 @@
   VarP "name"
 | AppP "exp" "exp"
 | LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1
 and pat3 =
   PVar "name"
 | PUnit
 | PPair "pat3" "pat3"
 binder
-  bp :: "pat3 \<Rightarrow> atom set"
+  bp' :: "pat3 \<Rightarrow> atom set"
 where
-  "bp (PVar x) = {atom x}"
-| "bp (PUnit) = {}"
-| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
-thm alpha_exp_raw_alpha_pat3_raw.intros
+  "bp' (PVar x) = {atom x}"
+| "bp' (PUnit) = {}"
+| "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
+thm alpha_exp_raw_alpha_pat3_raw_alpha_bp'_raw.intros
 
 (* example 6 from Peter Sewell's bestiary *)
 nominal_datatype exp6 =
@@ -452,7 +452,7 @@
   "bp6 (PVar' x) = {atom x}"
 | "bp6 (PUnit') = {}"
 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
-thm alpha_exp6_raw_alpha_pat6_raw.intros
+thm alpha_exp6_raw_alpha_pat6_raw_alpha_bp6_raw.intros
 
 (* example 7 from Peter Sewell's bestiary *)
 nominal_datatype exp7 =