theory TestMorePermimports "../NewParser"begintext {* "Weirdo" example from Peter Sewell's bestiary. This example is not covered by our binding specification.*}ML {* val _ = cheat_equivp := true *}atom_decl namenominal_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 p3thm 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]equivariance alpha_weird_rawend