--- a/Nominal/Test.thy	Wed Mar 03 19:10:40 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 15:31:21 2010 +0100
@@ -340,57 +340,60 @@
 
 atom_decl var
 atom_decl tvar
-atom_decl co
 
-datatype sort = 
-  TY tvar
-| CO co
-
-nominal_datatype kind = 
-  KStar
-| KFun kind kind
-| KEq kind kind
 
 (* there are types, coercion types and regular types *)
-(*
-nominal_datatype ty =
-  TVar tvar
-| TFun string "ty list"
-| TAll tvar kind_raw ty --"some binding"
-| TSym ty
-| TCir ty ty
-| TApp ty ty
-| TLeft ty
-| TRight ty
-| TEq ty
-| TRightc ty
-| TLeftc ty
-| TCoe ty ty
-*)
+nominal_datatype tkind = 
+  KStar
+| KFun "tkind" "tkind"
+and ckind =
+  CKEq "ty" "ty" 
+and ty =
+  TVar "tvar"
+| TC "string"
+| TApp "ty" "ty"
+| TFun "string" "ty list"
+| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
+| TEq "ty" "ty" "ty"
+and co =
+  CC "string"
+| CApp "co" "co"
+| CFun "string" "co list"
+| CAll tv::"tvar" "ckind" C::"co"  bind tv in C
+| CEq "co" "co" "co"
+| CSym "co"
+| CCir "co" "co"
+| CLeft "co"
+| CRight "co"
+| CSim "co"
+| CRightc "co"
+| CLeftc "co"
+| CCoe "co" "co"
+
+
 typedecl ty --"hack since ty is not yet defined"
 
 abbreviation 
   "atoms A \<equiv> atom ` A"
 
-(* does not work yet
 nominal_datatype trm =
-  Var var
-| LAM tv::tvar kind_raw t::trm   bind tv in t 
-| APP trm ty
-| Lam v::var ty t::trm       bind v in t
-| App trm trm
-| Let x::var ty trm t::trm   bind x in t
-| Case trm "assoc list"
-| Cast trm ty   --"ty is supposed to be a coercion type only"
+  Var "var"
+| C "string"
+| LAM tv::"tvar" "kind" t::"trm"   bind tv in t 
+| APP "trm" "ty"
+| Lam v::"var" "ty" t::"trm"       bind v in t
+| App "trm" "trm"
+| Let x::"var" "ty" "trm" t::"trm" bind x in t
+| Case "trm" "assoc list"
+| Cast "trm" "ty"                   --"ty is supposed to be a coercion type only"
 and assoc = 
-  A p::pat t::trm bind "bv p" in t 
+  A p::"pat" t::"trm" bind "bv p" in t 
 and pat = 
-  K string "(tvar \<times> kind_raw) list" "(var \<times> ty) list"
+  K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
 binder
  bv :: "pat \<Rightarrow> atom set"
 where
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-*)
 
 (*thm bv_raw.simps*)