--- a/Nominal/Ex/NoneExamples.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/NoneExamples.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -4,6 +4,40 @@
 
 atom_decl name
 
+
+text {* 
+  "Weirdo" example from Peter Sewell's bestiary. 
+
+  This example is not covered by our binding 
+  specification.
+
+*}
+
+nominal_datatype weird =
+  Foo_var "name"
+| Foo_pair "weird" "weird" 
+| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
+    bind x in p1 p2, 
+    bind y in p2 p3
+
+(* e1 occurs in two bodies *)
+
+nominal_datatype exp =
+  Var name
+| Pair exp exp
+| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1
+and pat =
+  PVar name
+| PUnit
+| PPair pat pat
+binder
+  bp :: "pat \<Rightarrow> atom list"
+where
+  "bp (PVar x) = [atom x]"
+| "bp (PUnit) = []"
+| "bp (PPair p1 p2) = bp p1 @ bp p2"
+
+
 (* this example binds bound names and
    so is not respectful *)
 (*