--- a/Nominal/ExCoreHaskell.thy	Mon Mar 29 16:56:59 2010 +0200
+++ b/Nominal/ExCoreHaskell.thy	Mon Mar 29 17:14:02 2010 +0200
@@ -29,11 +29,11 @@
   TsNil
 | TsCons "ty" "ty_lst"
 and co =
-  CC cvar
+  CVar "cvar"
 | CConst "string"
 | CApp "co" "co"
 | CFun "string" "co_lst"
-| CAll tv::"tvar" "ckind" C::"co"  bind tv in C
+| CAll cv::"cvar" "ckind" C::"co"  bind cv in C
 | CEq "ckind" "co"
 | CRefl "ty"
 | CSym "co"
@@ -50,7 +50,7 @@
 | CsCons "co" "co_lst"
 and trm =
   Var "var"
-| C "string"
+| K "string"
 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
 | LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
 | AppT "trm" "ty"
@@ -64,7 +64,7 @@
   ANil
 | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 and pat =
-  K "string" "tvtk_lst" "tvck_lst" "vt_lst"
+  Kpat "string" "tvtk_lst" "tvck_lst" "vt_lst"
 and vt_lst =
   VTNil
 | VTCons "var" "ty" "vt_lst"