--- a/Nominal/Ex/ExPS7.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExPS7.thy	Sun May 09 12:26:10 2010 +0100
@@ -1,3 +1,4 @@
+
 theory ExPS7
 imports "../NewParser"
 begin
@@ -6,25 +7,31 @@
 
 atom_decl name
 
-nominal_datatype exp7 =
-  EVar name
-| EUnit
-| EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e
+nominal_datatype exp =
+  Var name
+| Unit
+| Pair exp exp
+| LetRec l::"lrbs" e::"exp"  bind_set "bs l" in l e
 and lrb =
-  Assign name exp7
+  Assign name exp
 and lrbs =
   Single lrb
 | More lrb lrbs
 binder
-  b7 :: "lrb \<Rightarrow> atom set" and
-  b7s :: "lrbs \<Rightarrow> atom set"
+  b :: "lrb \<Rightarrow> atom set" and
+  bs :: "lrbs \<Rightarrow> atom set"
 where
-  "b7 (Assign x e) = {atom x}"
-| "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
+  "b (Assign x e) = {atom x}"
+| "bs (Single a) = b a"
+| "bs (More a as) = (b a) \<union> (bs as)"
+
+thm exp_lrb_lrbs.eq_iff
+thm exp_lrb_lrbs.supp
+
+declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
 
 end