diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Modules.thy
--- a/Nominal/Ex/Modules.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Modules.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -14,12 +14,12 @@
  mexp =
   Acc "path"
 | Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind (set) x in m
+| Funct x::"name" "sexp" m::"mexp"    binds (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"     binds (set) "cbinders c" in d
 and defn =
   Type "name" "ty"
 | Dty "name"
@@ -30,7 +30,7 @@
 | SFunc "name" "sexp" "sexp"
 and sbody =
   SEmpty
-| SSeq C::"spec" D::"sbody"    bind (set) "Cbinders C" in D
+| SSeq C::"spec" D::"sbody"    binds (set) "Cbinders C" in D
 and spec =
   Type1 "name"
 | Type2 "name" "ty"
@@ -46,7 +46,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"  binds (set) v in M
 | App' "trm" "trm"
 | Let' "body" "trm"
 binder