--- a/Nominal/NewParser.thy	Thu Apr 29 16:59:33 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Apr 29 17:52:19 2010 +0200
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "NewFv"
+        "Perm" "NewFv" "NewAlpha"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -278,8 +278,9 @@
   val lthy3 = Theory_Target.init NONE thy;
 
   val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (alpha, lthy5) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
+  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
 end
 *}
 
@@ -466,6 +467,7 @@
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
+thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros
 
 nominal_datatype exp =
   EVar name
@@ -516,6 +518,7 @@
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
+thm alpha_exp_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb_raw_alpha_lrbs_raw_alpha_pat_raw_alpha_b_lrbs_raw_alpha_b_pat_raw_alpha_b_fnclauses_raw_alpha_b_lrb_raw_alpha_b_fnclause_raw.intros
 
 nominal_datatype ty =
   Var "name"
@@ -524,6 +527,7 @@
 nominal_datatype tys =
   All xs::"name fset" ty::"ty_raw" bind_res xs in ty
 thm fv_tys_raw.simps
+thm alpha_tys_raw.intros
 
 (* some further tests *)