# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269950287 -7200
# Node ID 3d6df74fc934468a40f9fdf727d94a325ed1cc8e
# Parent  8c59c8a0721cef9e817c79994fd3ff237149b78f
Avoid mentioning other nominal datatypes as it makes things too complicated.

diff -r 8c59c8a0721c -r 3d6df74fc934 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 13:37:35 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 13:58:07 2010 +0200
@@ -1172,8 +1172,8 @@
   $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
   $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
      we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
-  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
-     with a free variable function @{text "fv\<^isup>\<alpha>"}\\\\
+%  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
+%     with a free variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}
@@ -1200,8 +1200,8 @@
   $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is 
      one of the datatypes
      we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
-  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
-     and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\
+%  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
+%     and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}
@@ -1245,8 +1245,8 @@
      has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
      alpha-equivalence for @{term "x\<^isub>j"}
      and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
-  $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes
-    the types being defined, raw)\\
+  $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being
+     defined\\
   $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
   \end{tabular}
   \end{center}
@@ -1259,10 +1259,11 @@
   @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if:
   \begin{center}
   \begin{tabular}{cp{7cm}}
-  $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\
-  $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not a nominal datatype and does not occur in @{text "rhs"}\\
-  $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a nominal datatype occuring in @{text "rhs"}
-    under the binding function @{text "bn\<^isub>m"}\\
+  $\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\
+  $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not of a type being defined
+    and does not occur in @{text "rhs"}\\
+  $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is of a type being defined
+    occuring in @{text "rhs"} under the binding function @{text "bn\<^isub>m"}\\
   $\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\
   \end{tabular}
   \end{center}