diff -r aa5059a00f41 -r 6fd3fc3254ee LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 17:16:11 2011 +0900
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 10:23:06 2011 +0200
@@ -1121,12 +1121,10 @@
   \hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"} 
      \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
   \isacommand{and} @{text pat} $=$\\
-  \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
-  \hspace{5mm}$\mid$~@{text "PVar name"}\\
+  \hspace{5mm}\phantom{$\mid$}~@{text "PVar name"}\\
   \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 
   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
-  \isacommand{where}~@{text "bn(PNil) = []"}\\
-  \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
+  \isacommand{where}~@{text "bn(PVar x) = [atom x]"}\\
   \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ 
   \end{tabular}}
   \end{equation}\smallskip
@@ -1972,7 +1970,6 @@
 
   \infer{@{text "P\<^bsub>pat\<^esub>"}}
   {\begin{array}{@ {}l@ {}}
-   @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
   \end{array}}\medskip\\
@@ -1985,7 +1982,6 @@
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
-   @{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\
    @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
   \end{array}}
@@ -2137,7 +2133,6 @@
    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\ 
    \hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
-   @{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\
    @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
   \end{array}}
@@ -2200,7 +2195,6 @@
 
   \infer{@{text "P\<^bsub>pat\<^esub>"}}
   {\begin{array}{@ {}l@ {}}
-   @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
   \end{array}}