diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -19,7 +19,7 @@
 | TC "string"
 | TApp "ty" "ty"
 | TFun "string" "ty_lst"
-| TAll tv::"tvar" "tkind" T::"ty"  bind (set) tv in T
+| TAll tv::"tvar" "tkind" T::"ty"  binds (set) tv in T
 | TEq "ckind" "ty"
 and ty_lst =
   TsNil
@@ -29,7 +29,7 @@
 | CConst "string"
 | CApp "co" "co"
 | CFun "string" "co_lst"
-| CAll cv::"cvar" "ckind" C::"co"  bind (set) cv in C
+| CAll cv::"cvar" "ckind" C::"co"  binds (set) cv in C
 | CEq "ckind" "co"
 | CRefl "ty"
 | CSym "co"
@@ -47,18 +47,18 @@
 and trm =
   Var "var"
 | K "string"
-| LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t
-| LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t
+| LAMT tv::"tvar" "tkind" t::"trm" binds (set) tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" binds (set) cv in t
 | AppT "trm" "ty"
 | AppC "trm" "co"
-| Lam v::"var" "ty" t::"trm"       bind (set) v in t
+| Lam v::"var" "ty" t::"trm"       binds (set) v in t
 | App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind (set) x in t
+| Let x::"var" "ty" "trm" t::"trm" binds (set) x in t
 | Case "trm" "assoc_lst"
 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 and assoc_lst =
   ANil
-| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
+| ACons p::"pat" t::"trm" "assoc_lst" binds "bv p" in t
 and pat =
   Kpat "string" "tvars" "cvars" "vars"
 and vars =