--- a/Nominal/Ex/ExPS6.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExPS6.thy	Sun May 09 12:26:10 2010 +0100
@@ -1,37 +1,42 @@
 theory ExPS6
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 6 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-(* The binding structure is too complicated, so equivalence the
-   way we define it is not true *)
+(* Is this binding structure supported - I think not 
+   because e1 occurs twice as body *)
 
-ML {* val _ = recursive := false  *}
-nominal_datatype exp6 =
-  EVar name
-| EPair exp6 exp6
-| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
-and pat6 =
-  PVar' name
-| PUnit'
-| PPair' pat6 pat6
+nominal_datatype exp =
+  Var name
+| Pair exp exp
+| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1
+and pat =
+  PVar name
+| PUnit
+| PPair pat pat
 binder
-  bp6 :: "pat6 \<Rightarrow> atom set"
+  bp :: "pat \<Rightarrow> atom list"
 where
-  "bp6 (PVar' x) = {atom x}"
-| "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
+  "bp (PVar x) = [atom x]"
+| "bp (PUnit) = []"
+| "bp (PPair p1 p2) = bp p1 @ bp p2"
 
-thm exp6_pat6.fv
-thm exp6_pat6.eq_iff
-thm exp6_pat6.bn
-thm exp6_pat6.perm
-thm exp6_pat6.induct
-thm exp6_pat6.distinct
-thm exp6_pat6.supp
+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.supp
+
+declare permute_exp_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
+
 
 end