diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Sat Aug 21 16:20:10 2010 +0800
@@ -20,7 +20,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"  bind (set) tv in T
 | TEq "ckind" "ty"
 and ty_lst =
   TsNil
@@ -30,7 +30,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"  bind (set) cv in C
 | CEq "ckind" "co"
 | CRefl "ty"
 | CSym "co"
@@ -48,13 +48,13 @@
 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" bind (set) tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" bind (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"       bind (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" bind (set) x in t
 | Case "trm" "assoc_lst"
 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 and assoc_lst =