--- a/Nominal/Ex/ExPS3.thy	Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExPS3.thy	Mon May 10 15:45:04 2010 +0200
@@ -11,29 +11,35 @@
 ML {* val _ = cheat_alpha_bn_rsp := true *}
 
 nominal_datatype exp =
-  VarP "name"
-| AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind_set x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
-and pat3 =
+  Var "name"
+| App "exp" "exp"
+| Lam x::"name" e::"exp" bind_set x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
+and pat =
   PVar "name"
 | PUnit
-| PPair "pat3" "pat3"
+| PPair "pat" "pat"
 binder
-  bp :: "pat3 \<Rightarrow> atom set"
+  bp :: "pat \<Rightarrow> atom set"
 where
   "bp (PVar x) = {atom x}"
 | "bp (PUnit) = {}"
 | "bp (PPair p1 p2) = bp p1 \<union> bp p2"
 
-thm exp_pat3.fv
-thm exp_pat3.eq_iff
-thm exp_pat3.bn
-thm exp_pat3.perm
-thm exp_pat3.induct
-thm exp_pat3.distinct
-thm exp_pat3.fv
-thm exp_pat3.supp(1-2)
+thm exp_pat.fv
+thm exp_pat.eq_iff
+thm exp_pat.bn
+thm exp_pat.perm
+thm exp_pat.induct
+thm exp_pat.distinct
+thm exp_pat.fv
+thm exp_pat.supp(1-2)
+
+declare permute_exp_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
+
 
 end