--- a/Nominal/Ex/TestMorePerm.thy	Thu Apr 08 11:40:13 2010 +0200
+++ b/Nominal/Ex/TestMorePerm.thy	Thu Apr 08 11:50:30 2010 +0200
@@ -2,13 +2,29 @@
 imports "../Parser"
 begin
 
-text {* weirdo example from Peter Sewell's bestiary *}
+text {* 
+  "Weirdo" example from Peter Sewell's bestiary. 
+
+  In case of deep binders, it is not coverd by our 
+  approach of defining alpha-equivalence with a 
+  single permutation.
+
+  Check whether it works with shallow binders as
+  defined below.
 
-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
-| WV "name"
-| WP "weird" "weird"
+*}
+ML {* val _ = cheat_equivp := true *}
+
+atom_decl name
+
+nominal_datatype foo =
+  Foo_var "name"
+| Foo_pair "foo" "foo" 
+| Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo"
+    bind x in p1, bind x in p2, 
+    bind y in p2, bind y in p3
+
+thm alpha_foo_raw.intros[no_vars]
 
 thm permute_weird_raw.simps[no_vars]
 thm alpha_weird_raw.intros[no_vars]