diff --git a/Monads.thy b/Monads.thy
index e5ea02b..86eec36 100644
--- a/Monads.thy
+++ b/Monads.thy
@@ -371,7 +371,7 @@ next
 next
   case goal4 then show ?case    
        apply (erule_tac Q="None = X" for X in contrapos_pp)
-       apply (erule_tac x="(aa,b)" and P="\<lambda> x. None \<noteq> split (\<lambda>out. k) x" in ballE)
+       apply (erule_tac x="(aa,b)" and P="\<lambda> x. None \<noteq> case_prod (\<lambda>out. k) x" in ballE)
        apply (auto simp: aux (*Option.not_None_eq*) image_def split_def intro!: rev_bexI)
      done
 next 
diff --git a/SeqComposition.thy b/SeqComposition.thy
index 9ee5dea..ac378b9 100644
--- a/SeqComposition.thy
+++ b/SeqComposition.thy
@@ -175,7 +175,7 @@ text{*
   flattening, we have four different forms of policy composition: *}
 definition
   comp_orA :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>"  (infixl "o'_orA" 55) where
-  "p2 o_orA p1 \<equiv> (map_option flat_orA) o (lift p2 o_m p1)"
+  "p2 o_orA p1 \<equiv> (map_option flat_orA) o (lift p2 \<circ>\<^sub>m p1)"
 
 notation (xsymbols)
   comp_orA  (infixl "\<circ>\<^sub>\<or>\<^sub>A" 55)
@@ -188,7 +188,7 @@ lemma mt_comp_orA[simp]:"\<emptyset> \<circ>\<^sub>\<or>\<^sub>A p = \<emptyset>
 
 definition
   comp_orD :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>"  (infixl "o'_orD" 55) where
-  "p2 o_orD p1 \<equiv> (map_option flat_orD) o (lift p2 o_m p1)"
+  "p2 o_orD p1 \<equiv> (map_option flat_orD) o (lift p2 \<circ>\<^sub>m p1)"
 
 notation (xsymbols)
   comp_orD  (infixl "\<circ>\<^sub>orD" 55)
@@ -201,7 +201,7 @@ lemma mt_comp_orD[simp]:"\<emptyset> o_orD p = \<emptyset>"
 
 definition
   comp_1 :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>"  (infixl "o'_1" 55) where
-  "p2 o_1 p1 \<equiv> (map_option flat_1) o (lift p2 o_m p1)"
+  "p2 o_1 p1 \<equiv> (map_option flat_1) o (lift p2 \<circ>\<^sub>m p1)"
 
 notation (xsymbols)
   comp_1  (infixl "\<circ>\<^sub>1" 55)
@@ -214,7 +214,7 @@ lemma mt_comp_1[simp]:"\<emptyset> \<circ>\<^sub>1 p = \<emptyset>"
 
 definition
   comp_2 :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>"  (infixl "o'_2" 55) where
-  "p2 o_2 p1 \<equiv> (map_option flat_2) o (lift p2 o_m p1)"
+  "p2 o_2 p1 \<equiv> (map_option flat_2) o (lift p2 \<circ>\<^sub>m p1)"
 
 notation (xsymbols)
   comp_2  (infixl "\<circ>\<^sub>2" 55)
diff --git a/ServiceExample.thy b/ServiceExample.thy
index 64edfba..7ed633d 100644
--- a/ServiceExample.thy
+++ b/ServiceExample.thy
@@ -114,7 +114,7 @@ lemmas PolSimps = valid_SE_def unit_SE_def bind_SE_def if_splits policy2MON_def
 lemma "SE_LR_RBAC_Policy ((createSCR alice Clerical patient1),\<sigma>0)= Some (deny ())"
 by (simp add: PolSimps)
 
-lemma exBool[simp]: "\<exists>a\<Colon>bool. a"  by auto
+lemma exBool[simp]: "\<exists>a::bool. a"  by auto
 
 lemma deny_allow[simp]: " \<lfloor>deny ()\<rfloor> \<notin> Some ` range allow"  by auto