--- a/Nominal/ExCoreHaskell.thy	Tue Mar 23 09:38:03 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Tue Mar 23 09:56:29 2010 +0100
@@ -9,8 +9,7 @@
 atom_decl var
 atom_decl tvar
 
-(* there are types, coercion types and regular types *)
-(* list-data-structure
+(* there are types, coercion types and regular types list-data-structure *)
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -20,13 +19,16 @@
   TVar "tvar"
 | TC "string"
 | TApp "ty" "ty"
-| TFun "string" "ty list"
+| TFun "string" "ty_lst"
 | TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
 | TEq "ty" "ty" "ty"
+and ty_lst =
+  TsNil
+| TsCons "ty" "ty_lst"
 and co =
   CC "string"
 | CApp "co" "co"
-| CFun "string" "co list"
+| CFun "string" "co_lst"
 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C
 | CEq "co" "co" "co"
 | CSym "co"
@@ -37,7 +39,11 @@
 | CRightc "co"
 | CLeftc "co"
 | CCoe "co" "co"
+and co_lst =
+  CsNil
+| CsCons "co" "co_lst"
 
+(*
 abbreviation
   "atoms A \<equiv> atom ` A"