--- a/Nominal/Ex/ExLeroy.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLeroy.thy	Sun May 09 12:26:10 2010 +0100
@@ -16,10 +16,10 @@
   Empty
 | Seq c::defn d::"body"     bind_set "cbinders c" in d
 and defn =
-  Type "name" "tyty"
+  Type "name" "ty"
 | Dty "name"
 | DStru "name" "mexp"
-| Val "name" "trmtrm"
+| Val "name" "trm"
 and sexp =
   Sig sbody
 | SFunc "name" "sexp" "sexp"
@@ -28,22 +28,22 @@
 | SSeq C::spec D::sbody    bind_set "Cbinders C" in D
 and spec =
   Type1 "name"
-| Type2 "name" "tyty"
+| Type2 "name" "ty"
 | SStru "name" "sexp"
-| SVal "name" "tyty"
-and tyty =
+| SVal "name" "ty"
+and ty =
   Tyref1 "name"
-| Tyref2 "path" "tyty"
-| Fun "tyty" "tyty"
+| Tyref2 "path" "ty"
+| Fun "ty" "ty"
 and path =
   Sref1 "name"
 | Sref2 "path" "name"
-and trmtrm =
+and trm =
   Tref1 "name"
 | Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm"  bind_set v in M
-| App' "trmtrm" "trmtrm"
-| Let' "body" "trmtrm"
+| Lam' v::"name" "ty" M::"trm"  bind_set v in M
+| App' "trm" "trm"
+| Let' "body" "trm"
 binder
     cbinders :: "defn \<Rightarrow> atom set"
 and Cbinders :: "spec \<Rightarrow> atom set"
@@ -57,15 +57,21 @@
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"
 
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)]
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
+
+declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
 
 end