diff -r 6f669bba4f0c -r 69472e74bd3b Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Mon Mar 29 16:44:26 2010 +0200
+++ b/Nominal/ExCoreHaskell.thy	Mon Mar 29 16:56:59 2010 +0200
@@ -7,6 +7,7 @@
 ML {* val _ = recursive := false *}
 
 atom_decl var
+atom_decl cvar
 atom_decl tvar
 
 (* there are types, coercion types and regular types list-data-structure *)
@@ -23,22 +24,24 @@
 | TApp "ty" "ty"
 | TFun "string" "ty_lst"
 | TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
-| TEq "ty" "ty" "ty"
+| TEq "ckind" "ty"
 and ty_lst =
   TsNil
 | TsCons "ty" "ty_lst"
 and co =
-  CC "string"
+  CC cvar
+| CConst "string"
 | CApp "co" "co"
 | CFun "string" "co_lst"
 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C
-| CEq "co" "co" "co"
+| CEq "ckind" "co"
+| CRefl "ty"
 | CSym "co"
-| CCir "co" "co" 
-(* At ??? *)
+| CCir "co" "co"
+| CAt "co" "ty"
 | CLeft "co"
 | CRight "co"
-| CSim "co"
+| CSim "co" "co"
 | CRightc "co"
 | CLeftc "co"
 | CCoe "co" "co"
@@ -49,8 +52,9 @@
   Var "var"
 | C "string"
 | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
-| LAMC tv::"tvar" "ckind" t::"trm" bind tv in t
-| APP "trm" "ty"
+| LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
+| AppT "trm" "ty"
+| AppC "trm" "co"
 | Lam v::"var" "ty" t::"trm"       bind v in t
 | App "trm" "trm"
 | Let x::"var" "ty" "trm" t::"trm" bind x in t
@@ -69,7 +73,7 @@
 | TVTKCons "tvar" "tkind" "tvtk_lst"
 and tvck_lst =
   TVCKNil
-| TVCKCons "tvar" "ckind" "tvck_lst"
+| TVCKCons "cvar" "ckind" "tvck_lst"
 binder
     bv :: "pat \<Rightarrow> atom list"
 and bv_vt :: "vt_lst \<Rightarrow> atom list"