--- a/Nominal/ExCoreHaskell.thy	Tue Mar 23 09:56:29 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Tue Mar 23 11:42:06 2010 +0100
@@ -10,6 +10,7 @@
 atom_decl tvar
 
 (* there are types, coercion types and regular types list-data-structure *)
+
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -17,18 +18,18 @@
   CKEq "ty" "ty"
 and ty =
   TVar "tvar"
-| TC "string"
+| TC "char"
 | TApp "ty" "ty"
-| TFun "string" "ty_lst"
+| TFun "char" "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"
+  CC "char"
 | CApp "co" "co"
-| CFun "string" "co_lst"
+| CFun "char" "co_lst"
 | CAll tv::"tvar" "ckind" C::"co"  bind tv in C
 | CEq "co" "co" "co"
 | CSym "co"
@@ -42,30 +43,44 @@
 and co_lst =
   CsNil
 | CsCons "co" "co_lst"
-
-(*
-abbreviation
-  "atoms A \<equiv> atom ` A"
-
-nominal_datatype trm =
+and trm =
   Var "var"
-| C "string"
-| LAM tv::"tvar" "kind" t::"trm"   bind tv in t
+| C "char"
+| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
+| LAMC tv::"tvar" "ckind" 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
+| Case "trm" "assoc_lst"
+| Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
+and assoc_lst =
+  ANil
+| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
 and pat =
-  K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
+  K "char" "tvtk_lst" "tvck_lst" "vt_lst"
+and tvtk_lst =
+  TVTKNil
+| TVTKCons "tvar" "tkind" "tvtk_lst"
+and tvck_lst =
+  TVCKNil
+| TVCKCons "tvar" "ckind" "tvck_lst"
+and vt_lst =
+  VTNil
+| VTCons "var" "ty" "vt_lst"
 binder
- bv :: "pat \<Rightarrow> atom set"
+    bv :: "pat \<Rightarrow> atom set"
+(*and bv_vt :: "vt_lst \<Rightarrow> atom set"
+and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set"
+and bv_tvck :: "tvck_lst \<Rightarrow> atom set"*)
 where
- "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-*)
+  "bv (K s tvts tvcs vs) = {}" (*(bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs) *)
+(*| "bv_vt VTNil = {}"
+| "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t"
+| "bv_tvtk TVTKNil = {}"
+| "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t"
+| "bv_tvck TVCKNil = {}"
+| "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"*)
 
 end
 

--- a/Nominal/Fv.thy	Tue Mar 23 09:56:29 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 23 11:42:06 2010 +0100
@@ -841,14 +841,13 @@
 
 ML {*
 fun equivp_tac reflps symps transps =
-  let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in
+  (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
   simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
   THEN' rtac conjI THEN' rtac allI THEN'
   resolve_tac reflps THEN'
   rtac conjI THEN' rtac allI THEN' rtac allI THEN'
   resolve_tac symps THEN'
   rtac @{thm transpI} THEN' resolve_tac transps
-  end
 *}
 
 ML {*