--- a/Nominal/Ex/TestMorePerm.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/TestMorePerm.thy	Sun May 09 12:26:10 2010 +0100
@@ -1,35 +1,35 @@
 theory TestMorePerm
-imports "../Parser"
+imports "../NewParser"
 begin
 
 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.
+  This example is not covered by our binding 
+  specification.
 
 *}
 ML {* val _ = cheat_equivp := true *}
 
 atom_decl name
 
-nominal_datatype foo =
+nominal_datatype weird =
   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
+| 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
 
-thm alpha_foo_raw.intros[no_vars]
+thm alpha_weird_raw.intros[no_vars]
 
 thm permute_weird_raw.simps[no_vars]
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
+declare permute_weird_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_weird_raw
+
 
 end