diff --git a/UPF/ElementaryPolicies.thy b/UPF/ElementaryPolicies.thy
index ad05574..5299f40 100644
--- a/UPF/ElementaryPolicies.thy
+++ b/UPF/ElementaryPolicies.thy
@@ -139,13 +139,13 @@ definition
 
 text{* ... and resulting properties: *}
 
-lemma "A\<^sub>I  \<Oplus> empty  = A\<^sub>I"
+lemma "A\<^sub>I  \<Oplus> Map.empty  = A\<^sub>I"
   by simp 
   
-lemma "A\<^sub>f f  \<Oplus> empty  = A\<^sub>f f"
+lemma "A\<^sub>f f  \<Oplus> Map.empty  = A\<^sub>f f"
   by simp 
   
-lemma "allow_pfun empty = empty"
+lemma "allow_pfun Map.empty = Map.empty"
   apply (rule ext)
   apply (simp add: allow_pfun_def)
   done
diff --git a/UPF/Monads.thy b/UPF/Monads.thy
index 94ca85a..e29db24 100644
--- a/UPF/Monads.thy
+++ b/UPF/Monads.thy
@@ -221,7 +221,7 @@ where "mbind' [] iostep \<sigma> = Some([], \<sigma>)" |
                 (case iostep a \<sigma> of 
                      None   \<Rightarrow> None
                   |  Some (out, \<sigma>') \<Rightarrow> (case mbind H iostep \<sigma>' of 
-                                          None    \<Rightarrow> None   (*  fail-strict *) 
+                                          None    \<Rightarrow> None   \<comment> \<open>fail-strict\<close>
                                         | Some(outs,\<sigma>'') \<Rightarrow> Some(out#outs,\<sigma>'')))"
 
 text{* 
diff --git a/UPF/Normalisation.thy b/UPF/Normalisation.thy
index 2730764..ecae0e4 100644
--- a/UPF/Normalisation.thy
+++ b/UPF/Normalisation.thy
@@ -267,7 +267,7 @@ text{*
 definition prod_2_list :: "[('\<alpha> \<mapsto>'\<beta>), (('\<gamma> \<mapsto>'\<delta>) list)] \<Rightarrow> 
                   (('\<beta> \<times> '\<delta>) \<Rightarrow> 'y) \<Rightarrow> ('x \<Rightarrow> ('\<alpha> \<times> '\<gamma>)) \<Rightarrow> 
                   (('x \<mapsto> 'y) list)" (infixr "\<Otimes>\<^sub>2\<^sub>L" 55) where 
-  "x \<Otimes>\<^sub>2\<^sub>L y =  (\<lambda> d r. (x \<Otimes>\<^sub>L y) (op \<Otimes>\<^sub>2) d r)"  
+  "x \<Otimes>\<^sub>2\<^sub>L y =  (\<lambda> d r. (x \<Otimes>\<^sub>L y) (\<Otimes>\<^sub>2) d r)"  
   
 lemma list2listNMT:  "x \<noteq> [] \<Longrightarrow> map sem x \<noteq> []"
   apply (case_tac x)
@@ -288,25 +288,25 @@ definition is_distr where
 definition is_strict where
  "is_strict p = (\<lambda> r d. \<forall> P1. (r o_f (p P1 \<emptyset> \<circ> d)) = \<emptyset>)"
 
-lemma is_distr_orD: "is_distr (op \<Otimes>\<^sub>\<or>\<^sub>D) d r"
+lemma is_distr_orD: "is_distr (\<Otimes>\<^sub>\<or>\<^sub>D) d r"
   apply (simp add: is_distr_def)
   apply (rule allI)+
   apply (rule distr_orD)
   apply (simp)
   done
     
-lemma is_strict_orD: "is_strict (op \<Otimes>\<^sub>\<or>\<^sub>D) d r"
+lemma is_strict_orD: "is_strict (\<Otimes>\<^sub>\<or>\<^sub>D) d r"
   apply (simp add: is_strict_def)
   apply (simp add: policy_range_comp_def)
   done
     
-lemma is_distr_2: "is_distr (op \<Otimes>\<^sub>2) d r"
+lemma is_distr_2: "is_distr (\<Otimes>\<^sub>2) d r"
   apply (simp add: is_distr_def)
   apply (rule allI)+
   apply (rule distr_or2)
   by simp
     
-lemma is_strict_2: "is_strict (op \<Otimes>\<^sub>2) d r"
+lemma is_strict_2: "is_strict (\<Otimes>\<^sub>2) d r"
   apply (simp only: is_strict_def)
   apply simp
   apply (simp add: policy_range_comp_def)
@@ -323,8 +323,8 @@ lemma notDom: "x \<in> dom A \<Longrightarrow> \<not> A x = None"
 text{* 
   The following theorems are crucial: they establish the correctness of the distribution.
 *}
-lemma Norm_Distr_1:  "((r o_f (((op \<Otimes>\<^sub>1) P1 (list2policy P2)) o d)) x = 
-                                                   ((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>1) r d)) x))"
+lemma Norm_Distr_1:  "((r o_f (((\<Otimes>\<^sub>1) P1 (list2policy P2)) o d)) x = 
+                                                   ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>1) r d)) x))"
 proof (induct P2) 
   case Nil show ?case
     by (simp add: policy_range_comp_def  list2policy_def) 
@@ -341,8 +341,8 @@ next
   qed
 qed
   
-lemma Norm_Distr_2: "((r o_f (((op \<Otimes>\<^sub>2) P1 (list2policy P2)) o d)) x = 
-                               ((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>2) r d)) x))"proof (induct P2) 
+lemma Norm_Distr_2: "((r o_f (((\<Otimes>\<^sub>2) P1 (list2policy P2)) o d)) x = 
+                               ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>2) r d)) x))"proof (induct P2) 
   case Nil show ?case
     by (simp add: policy_range_comp_def  list2policy_def) 
 next
@@ -358,8 +358,8 @@ next
   qed
 qed
   
-lemma Norm_Distr_A: "((r o_f (((op \<Otimes>\<^sub>\<or>\<^sub>A) P1 (list2policy P2)) o d)) x = 
-                                                 ((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>\<or>\<^sub>A) r d)) x))"
+lemma Norm_Distr_A: "((r o_f (((\<Otimes>\<^sub>\<or>\<^sub>A) P1 (list2policy P2)) o d)) x = 
+                                                 ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>A) r d)) x))"
 proof (induct P2) 
   case Nil show ?case
     by (simp add: policy_range_comp_def  list2policy_def) 
@@ -377,8 +377,8 @@ next
 qed
 
   
-lemma Norm_Distr_D: "((r o_f (((op \<Otimes>\<^sub>\<or>\<^sub>D) P1 (list2policy P2)) o d)) x = 
-                                                  ((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>\<or>\<^sub>D) r d)) x))"
+lemma Norm_Distr_D: "((r o_f (((\<Otimes>\<^sub>\<or>\<^sub>D) P1 (list2policy P2)) o d)) x = 
+                                                  ((list2policy ((P1 \<Otimes>\<^sub>L P2) (\<Otimes>\<^sub>\<or>\<^sub>D) r d)) x))"
 proof (induct P2) 
   case Nil show ?case
     by (simp add: policy_range_comp_def  list2policy_def) 
diff --git a/UPF/ROOT b/UPF/ROOT
index c418faa..78db805 100644
--- a/UPF/ROOT
+++ b/UPF/ROOT
@@ -2,7 +2,7 @@ chapter AFP
 
 session "UPF" (AFP) = HOL +
   description {* The Unified Policy Framework (UPF) *}
-  options [timeout=300]
+  options [timeout = 300]
   theories
     Monads
     UPF
diff --git a/UPF/Service.thy b/UPF/Service.thy
index 4479260..5160693 100644
--- a/UPF/Service.thy
+++ b/UPF/Service.thy
@@ -423,7 +423,7 @@ fun OpSuccessSigma :: "(Operation \<times> \<Sigma>) \<rightharpoonup> \<Sigma>"
                    (case S p of \<lfloor>lrs\<rfloor>  \<Rightarrow> (case (lrs lr_id) of 
                                                \<bottom>  \<Rightarrow> \<lfloor>S(p\<mapsto>(lrs(lr_id\<mapsto>us)))\<rfloor>                        
                                              | \<lfloor>x\<rfloor> \<Rightarrow> \<lfloor>S\<rfloor>)
-                              | \<bottom> \<Rightarrow> \<lfloor>S(p\<mapsto>(empty(lr_id\<mapsto>us)))\<rfloor>)"
+                              | \<bottom> \<Rightarrow> \<lfloor>S(p\<mapsto>(Map.empty(lr_id\<mapsto>us)))\<rfloor>)"
   |"OpSuccessSigma (removeLR u r p lr_id,S) = 
                    (case S p of Some lrs \<Rightarrow> \<lfloor>S(p\<mapsto>(lrs(lr_id:=\<bottom>)))\<rfloor>
                               | \<bottom> \<Rightarrow> \<lfloor>S\<rfloor>)"
diff --git a/UPF/ServiceExample.thy b/UPF/ServiceExample.thy
index 97d0c92..f584640 100644
--- a/UPF/ServiceExample.thy
+++ b/UPF/ServiceExample.thy
@@ -59,7 +59,7 @@ definition patient1 :: patient where "patient1 = 5"
 definition patient2 :: patient where "patient2 = 6"
 
 definition UC0 :: \<upsilon> where
- "UC0 = empty(alice\<mapsto>Nurse)(bob\<mapsto>ClinicalPractitioner)(charlie\<mapsto>Clerical)"
+ "UC0 = Map.empty(alice\<mapsto>Nurse)(bob\<mapsto>ClinicalPractitioner)(charlie\<mapsto>Clerical)"
 
 definition entry1  :: entry where
  "entry1 = (Open,alice, dummyContent)"
@@ -77,13 +77,13 @@ definition SCR2 :: SCR where
  "SCR2 =  (Map.empty)"
 
 definition Spine0 :: DB where
- "Spine0 = empty(patient1\<mapsto>SCR1)(patient2\<mapsto>SCR2)"
+ "Spine0 = Map.empty(patient1\<mapsto>SCR1)(patient2\<mapsto>SCR2)"
 
 definition LR1 :: LR where
- "LR1 =(empty(1\<mapsto>{alice}))"
+ "LR1 =(Map.empty(1\<mapsto>{alice}))"
 
 definition \<Sigma>0 :: \<Sigma> where
- "\<Sigma>0 = (empty(patient1\<mapsto>LR1))"
+ "\<Sigma>0 = (Map.empty(patient1\<mapsto>LR1))"
 
 subsection {* The Initial System State *}
 definition \<sigma>0 :: "DB \<times> \<Sigma>\<times>\<upsilon>" where
diff --git a/UPF/UPFCore.thy b/UPF/UPFCore.thy
index 9f4ad41..fba5c4e 100644
--- a/UPF/UPFCore.thy
+++ b/UPF/UPFCore.thy
@@ -135,10 +135,10 @@ translations
   "_MapUpd m (_Maplets xy ms)"   \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
   "_MapUpd m (_policylet1 x y)"  \<rightleftharpoons> "m(x := CONST Some (CONST allow y))"
   "_MapUpd m (_policylet2 x y)"  \<rightleftharpoons> "m(x := CONST Some (CONST deny y))"
-  "\<emptyset>"                            \<rightleftharpoons> "CONST empty" 
+  "\<emptyset>"                            \<rightleftharpoons> "CONST Map.empty" 
 
 text{* Here are some lemmas essentially showing syntactic equivalences: *}
-lemma test: "empty(x\<mapsto>\<^sub>+a, y\<mapsto>\<^sub>-b) = \<emptyset>(x \<mapsto>\<^sub>+ a, y \<mapsto>\<^sub>- b)"   by simp
+lemma test: "\<emptyset>(x\<mapsto>\<^sub>+a, y\<mapsto>\<^sub>-b) = \<emptyset>(x \<mapsto>\<^sub>+ a, y \<mapsto>\<^sub>- b)"   by simp
 
 lemma test2: "p(x\<mapsto>\<^sub>+a,x\<mapsto>\<^sub>-b) = p(x\<mapsto>\<^sub>-b)"   by simp