--- a/Nominal/Test.thy	Tue Mar 02 18:48:20 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 18:57:26 2010 +0100
@@ -2,6 +2,20 @@
 imports "Parser"
 begin
 
+text {* weirdo example from Peter Sewell's bestiary *}
+
+nominal_datatype weird =
+  WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
+    bind x in p1, bind x in p2, bind y in p2, bind y in p3
+| WVar "name"
+| WPair "weird" "weird"
+
+thm alpha_weird_raw.intros[no_vars]
+thm fv_weird_raw.simps[no_vars]
+(* Potential problem: Is it correct that in the fv-function 
+the first two terms are created? Should be ommitted. Also
+something wrong with the permutations. *)
+
 text {* example 1 *}
 
 nominal_datatype lam =
@@ -46,6 +60,9 @@
 | "f (PS x) = {atom x}"
 | "f (PD x y) = {atom x, atom y}"
 
+
+thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars]
+thm fv_trm'_raw_fv_pat'_raw.simps[no_vars]
 thm f_raw.simps
 
 nominal_datatype trm0 =