--- a/Nominal/Test.thy	Tue Mar 09 17:25:35 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 09 22:08:38 2010 +0100
@@ -66,8 +66,9 @@
   f::"pat' \<Rightarrow> atom set"
 where 
   "f PN = {}"
+| "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
-| "f (PD x y) = {atom x, atom y}"
+
 
 (* compat should be
 compat (PN) pi (PN) == True