--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Oct 27 13:54:18 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Oct 27 14:15:54 2010 -0700
@@ -39,7 +39,7 @@
     | x##xs => (flift1
             (%p.(If Def ((fst p)~:actions sig)
                  then Def (s=(snd p))
-                 else TT fi)
+                 else TT)
                 andalso (h$xs) (snd p))
              $x)
    )))"
@@ -137,7 +137,7 @@
      | x##xs => (flift1
              (%p.(If Def ((fst p)~:actions sig)
                   then Def (s=(snd p))
-                  else TT fi)
+                  else TT)
                  andalso (stutter2 sig$xs) (snd p))
               $x)
             ))"