--- a/Nominal/Ex/Modules.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Modules.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -7,15 +7,16 @@
 
 atom_decl name
 
-nominal_datatype mexp =
+nominal_datatype modules: 
+ mexp =
   Acc "path"
 | Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind_set x in m
+| Funct x::"name" "sexp" m::"mexp"    bind (set) x in m
 | FApp "mexp" "path"
 | Ascr "mexp" "sexp"
 and body =
   Empty
-| Seq c::defn d::"body"     bind_set "cbinders c" in d
+| Seq c::"defn" d::"body"     bind (set) "cbinders c" in d
 and defn =
   Type "name" "ty"
 | Dty "name"
@@ -26,7 +27,7 @@
 | SFunc "name" "sexp" "sexp"
 and sbody =
   SEmpty
-| SSeq C::spec D::sbody    bind_set "Cbinders C" in D
+| SSeq C::"spec" D::"sbody"    bind (set) "Cbinders C" in D
 and spec =
   Type1 "name"
 | Type2 "name" "ty"
@@ -42,7 +43,7 @@
 and trm =
   Tref1 "name"
 | Tref2 "path" "name"
-| Lam' v::"name" "ty" M::"trm"  bind_set v in M
+| Lam' v::"name" "ty" M::"trm"  bind (set) v in M
 | App' "trm" "trm"
 | Let' "body" "trm"
 binder
@@ -58,15 +59,16 @@
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"
 
-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)]
+
+thm modules.distinct
+thm modules.induct
+thm modules.exhaust
+thm modules.fv_defs
+thm modules.bn_defs
+thm modules.perm_simps
+thm modules.eq_iff
+thm modules.fv_bn_eqvt
+thm modules.size_eqvt