--- 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"

--- a/Paper/Paper.thy	Mon Mar 29 16:56:59 2010 +0200
+++ b/Paper/Paper.thy	Mon Mar 29 17:14:02 2010 +0200
@@ -360,41 +360,44 @@
   \begin{figure}
   \begin{boxedminipage}{\linewidth}
   \begin{center}
-  \begin{tabular}{r@ {\hspace{2mm}}cl}
+  \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
   \multicolumn{3}{@ {}l}{Type Kinds}\\
-  @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\medskip\\
+  @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
   \multicolumn{3}{@ {}l}{Coercion Kinds}\\
-  @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\medskip\\
+  @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
   \multicolumn{3}{@ {}l}{Types}\\
   @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} 
-  @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\medskip\\
+  @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
   \multicolumn{3}{@ {}l}{Coercion Types}\\
   @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
-  @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> |"}\\
-  & & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> |"}\\
-  & & @{text "left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 |"}\\
-  & & @{text "rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\medskip\\
+  @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
+  & @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
+  & @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
   \multicolumn{3}{@ {}l}{Terms}\\
-  @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma> |"}\\
-  & & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 |"}\\
-  & & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\medskip\\
+  @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+  & @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+  & @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
   \multicolumn{3}{@ {}l}{Patterns}\\
-  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
+  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
   \multicolumn{3}{@ {}l}{Constants}\\
-  @{text C} & & coercion constants\\
-  @{text T} & & value type constructors\\
-  @{text "S\<^isub>n"} & & n-ary type functions\\
-  @{text K} & & data constructors\medskip\\
+  & @{text C} & coercion constants\\
+  & @{text T} & value type constructors\\
+  & @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
+  & @{text K} & data constructors\smallskip\\
   \multicolumn{3}{@ {}l}{Variables}\\
-  @{text a} & & type variables\\
-  @{text c} & & coercion variables\\
-  @{text x} & & term variables\\
+  & @{text a} & type variables\\
+  & @{text c} & coercion variables\\
+  & @{text x} & term variables\\
   \end{tabular}
   \end{center}
   \end{boxedminipage}
-  \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as \emph{Core-Haskell}
-   \cite{CoreHaskell}. In this version of Core-Haskell we made a modification by 
-  separating completely the grammars for type kinds and coercion types.\label{corehas}}
+  \caption{The term-language of System @{text "F\<^isub>C"}
+  \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
+  version of the term-language we made a modification by separating the
+  grammars for type and coercion kinds, as well as types and coercion
+  types. For this paper the interesting term-constructor is @{text "\<CASE>"}
+  involving the binding of multiple type-, coercion- and term-variables from
+  patterns.\label{corehas}}
   \end{figure}
 *}