diff -r 021672ec28f5 -r 137358bd4921 Tainted_prop.thy
--- a/Tainted_prop.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/Tainted_prop.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -15,9 +15,9 @@
      (if (O_file f) \<in> Tainted s then Tainted s \<union> {O_proc p} else Tainted s)"
 | "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}"
 | "Tainted (Ptrace p p' # s) = 
-     (if (O_proc p) \<in> Tainted s 
+     (if (O_proc p \<in> Tainted s)
       then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
-      else if (O_proc p') \<in> Tainted s 
+      else if (O_proc p' \<in> Tainted s)
            then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
                 else Tainted s)"
 | "Tainted (Exit p # s) = Tainted s - {O_proc p}"