--- a/Nominal/Ex/CoreHaskell.thy	Mon May 10 15:45:04 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Mon May 10 18:29:45 2010 +0200
@@ -18,7 +18,7 @@
 | TC "string"
 | TApp "ty" "ty"
 | TFun "string" "ty_lst"
-| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
+| TAll tv::"tvar" "tkind" T::"ty"  bind_set tv in T
 | TEq "ckind" "ty"
 and ty_lst =
   TsNil
@@ -28,7 +28,7 @@
 | CConst "string"
 | CApp "co" "co"
 | CFun "string" "co_lst"
-| CAll cv::"cvar" "ckind" C::"co"  bind cv in C
+| CAll cv::"cvar" "ckind" C::"co"  bind_set cv in C
 | CEq "ckind" "co"
 | CRefl "ty"
 | CSym "co"
@@ -46,13 +46,13 @@
 and trm =
   Var "var"
 | K "string"
-| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
-| LAMC cv::"cvar" "ckind" t::"trm" bind 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 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 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 =