diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/NoneExamples.thy
--- a/Nominal/Ex/NoneExamples.thy	Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/NoneExamples.thy	Wed Dec 22 21:13:44 2010 +0000
@@ -3,7 +3,7 @@
 begin
 
 text {*
-  This example is not covered by our binding 
+  These examples are not covered by our binding 
   specification.
 *}
 
@@ -25,7 +25,7 @@
 *)
 
 text {* 
-  this example binds bound names and therefore the 
+  This example binds bound names and therefore the 
   fv-function is not respectful - the proof just fails.
 *}
 
@@ -43,7 +43,7 @@
 *)
 
 text {* 
-  this example uses "-" in the binding function; 
+  This example uses "-" in the binding function; 
   at the moment this is unsupported 
 *}
 
@@ -61,7 +61,7 @@
 *)
 
 text {* 
-  again this example binds bound names - so not respectful
+  Again this example binds bound names - so is not respectful
 *}
 
 (*
@@ -73,10 +73,33 @@
 binder
   bv :: "trm \<Rightarrow> atom set"
 where
-  "bv (Vam x) = {}"
+  "bv (Var x) = {}"
 | "bv (Lam x b) = {atom x}"
 *)
 
+text {*
+  This example has mal-formed deep recursive binders.
+
+  - Bla1: recursive deep binder used twice
+  - Bla2: deep binder used recursively and non-recursively
+  - Bla3: x used in recursive deep binder and somewhere else
+*}
+
+(*
+nominal_datatype trm =
+  Var "name"
+and bla =
+  App "trm" "trm"
+| Bla1 f::"trm" s1::"trm" s2::"trm"  bind "bv f" in s1 f,  bind "bv f" in s2 f
+| Bla2 f::"trm" s1::"trm" s2::"trm"  bind "bv f" in s1,  bind "bv f" in s2 f
+| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" bind "bv f" x in s1 f, bind y x in s2 
+binder
+  bv :: "trm \<Rightarrow> atom list"
+where
+  "bv (Var a) = [atom a]"
+*)
+
+
 end